Branch: master
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
Benton2004.Aux.fst
Benton2004.Aux.fst.hints
Benton2004.Aux.fsti
Benton2004.DDCC.Examples.fst
Benton2004.DDCC.Examples.fst.hints
Benton2004.DDCC.fst
Benton2004.DDCC.fst.hints
Benton2004.RHL.Derived.fst
Benton2004.RHL.Derived.fst.hints
Benton2004.RHL.Examples.fst
Benton2004.RHL.Examples.fst.hints
Benton2004.RHL.Examples2.fst
Benton2004.RHL.Examples2.fst.hints
Benton2004.RHL.fst
Benton2004.RHL.fst.hints
Benton2004.SmithVolpano.fst
Benton2004.SmithVolpano.fst.hints
Benton2004.fst
Benton2004.fst.hints
Bijection.fst
Bijection.fst.hints
ElGamal.fst
ElGamal.fst.hints
Equivalence.fst
Equivalence.fst.hints
IfcComposeReify.fst
IfcComposeReify.fst.hints
IfcDeclassify.fst
IfcDeclassify.fst.hints
IfcDelimitedRelease.fst
IfcDelimitedRelease.fst.hints
IfcDelimitedReleaseReify.fst
IfcDelimitedReleaseReify.fst.hints
IfcExample.fst
IfcExample.fst.hints
IfcExampleReify0.fst
IfcExampleReify0.fst.hints
IfcExampleReify1.fst
IfcExampleReify1.fst.hints
IfcExampleReify2.fst
IfcExampleReify2.fst.hints
IfcExampleReify3.fst
IfcExampleReify3.fst.hints
IfcMonitor.fst
IfcMonitorTest.fst
IfcRecursiveHeapReify.fst
IfcRecursiveReify.fst
IfcRecursiveReify.fst.hints
IfcReificationRegressionTest.fst
IfcReificationRegressionTest.fst.hints
IfcRules.fst
IfcRules.fst.hints
IfcRulesReify.fst
IfcRulesReify.fst.hints
IfcTypechecker.fst
IfcTypechecker.fst.hints
Loops.fst
Loops.fst.hints
Makefile
Memo.fst
Memo.fst.hints
NetKat.fst
NetKat.fst.hints
OTP.fst
OTP.fst.hints
OneTimePad.fst
OneTimePad.fst.hints
Point.fst
Point.fst.hints
ProgramEquivalence.fst
ProgramEquivalence.fst.hints
ProgramOptimizations.fst
ProgramOptimizations.fst.hints
README.md
RandomTapes.fst
RandomTapes.fst.hints
Recursive.fst
Recursive.fst.hints
ReifyLong.fst
ReifyLong.fst.hints
Rel.fst
Rel.fst.hints
StRel.fst
StRel.fst.hints
Swap.fst
Swap.fst.hints
UnionFind.Forest.fst
UnionFind.Forest.fst.hints
UnionFind.Functions.fst
UnionFind.Functions.fst.hints
UnionFind.fst
UnionFind.fst.hints
While.fst
While.fst.hints
WhileReify.fst
WhileReify.fst.hints
label.fst
sections.csv
setup_timings.py

README.md

Examples for A Monadic Framework for Relational Verification

All the examples are in the rel subdir, but some use things in dm4free internally. This is known to work with the c_relational-ci_r3 branch of F*, commit 380997df in particular. This requires Z3 version 4.5.1 to verify (in particular IfcMonitor is known to fail with Z3 4.5.0).

Section 1

  • Loops.fst: sum_up/sum_dn from 1.1

Section 2

  • Loops.fst: sum_up/sum_dn from 2.4

Section 3

  • Swap.fst: all the program transformations on commands from 3.2

  • Benton2004.fst, Benton2004.RHL.fst and Benton2004.RHL.Examples2.fst: relational Hoare logic by Benton (2004), model, soundness proofs and examples as described in 3.3 (other files Benton2004.* model the rest of Benton's paper)

Section 4

  • IfcRulesReify.fst: the IFC type system from 4.1
  • IfcMonitor.fst and IfcMonitorTest.fst: the dynamic IFC monitor from 4.2
  • IfcTypechecker.fst: the IFC typecheckers from 4.1 and 4.3
  • IfcExampleReify2.fst: the simple program from 4.3 and its hybrid proof
  • IfcDelimitedRelease.fst: the delimited release definition from 4.4
  • IfcDeclassify.fst: the simple definition of when declassification from 4.4

Section 5

  • ../dm4free/FStar.DM4F.Heap.Random.fst,../dm4free/FStar.DM4F.Random.fst: definition of the RAND effect in 5.1 and proof of mass_leq lemma in 5.2
  • OTP.fst: proof of perfect secrecy of one-time pad in 5.2
  • ../dm4free/FStar.DM4F.OTP.Heap.fst,../dm4free/FStar.DM4F.OTP.Random.fst: the variant of the RAND effect in 5.1 used in the proof in 5.3
  • ElGamal.fst: the proof of the secrecy lemma in 5.3

Section 6

  • Memo.fst: the memoization example from 6.1
  • UnionFind.fst: the union find example from 6.2