No-send-after-read

This verification example covers a common security property: a secure device does not send out data when it received privacy-sensitive information. Model-based abstraction is used to verify that the program adheres to a process algebra abstraction, which does not perform a 'send' action after receiving privacy-sensitive information.

General information

ID60
Articlenone
Back-endSilicon
LanguageJava
FeaturesFutures
Sources
Path to example filefutures/NoSendAfterRead.java
Date2017-06-16

Statistical information

Lines of code127 lines (comments not included)
Lines of specification66 lines (51.97% of the total)
Computation time25291 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.