ProVerif proofs for paper "A Malware-Tolerant, Self-Healing Industrial Control System Framework"
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
proofs
.gitignore
LICENSE
README.md
run_all.sh

README.md

ProVerif Proofs for Self-Healing Industrial Control System

Paper: A Malware-Tolerant, Self-Healing Industrial Control System Framework
Authors: Michael Denzel, Mark Ryan, Eike Ritter
Date: 2017-03-17

See also: https://github.com/mdenzel/self-healing_FreeRTOS for the ARM TrustZone implementation of the self-healing Real-Time Operating System.

Quick Start

REMARK: ALL PROOFS REQUIRE PROVERIF v. 1.96!

Simply run the shellscript in the command-line:

	$ sh ./run_all.sh

(tested on Fedora 25; ProVerif v. 1.96)

Keywords:

plc          = Programmable Logic Controller
2oo3         = 2-out-of-3 circuit
r            = reset circuit
success      = proof reaches the end of the protocol
YES          = ProVerif file proves the property
NO           = ProVerif file does not prove the property

There is also a self-explanatory CONFIG section in run_all.sh.

Running ProVerif Manually

Since there are 24 proofs for every configuration, we generate the proofs from the *.gen files using the C-pre-processor. The run_all.sh script has an option (ONLY_GENERATE) to generate the proofs without running them.

Afterwards the ProVerif files are in the sub-folder ./proofs/proofs-*. They can be run separately and are named by the compromised devices.

plc  = compromised Programmable Logic Controller (PLC)
2oo3 = compromised 2-out-of-3 circuit
r    = compromised reset circuit

To run a proof, execute for example the following:

    $ proverif ./proofs/proofs-selfhealing_proverif.gen/24_all_compromised.pv

REMARK: success is a (dummy) secret which gets leaked at the end of the protocol to indicate that it ran through. Thus, when running manually, ProVerif should return false:

The attacker has the message success in phase 1.
A trace has been found.
RESULT not attacker_p1(success[]) is false.

License

All provided files in this repository are under the GNU General Public License 2.0 or later.