Modular Product Programs

Examples from the paper "Modular Product Programs", presented at ESOP 2018, and the extended version of the paper submitted to ACM ToPLAS.

Secure Information Flow

Examples for proving secure information flow, using information flow specifications.

Banerjee

Example from 'Secure Information Flow and Pointer Confinement in a Java-like Language', A. Banerjee and D. A. Naumann, CSFW 2002

Constanzo

Example from 'A Separation Logic for Enforcing Declarative Information Flow Control Policies', D. Costanzo and Z. Shao, POST 2014

Darvas

Example from 'A Theorem Proving Approach to Analysis of Secure Information Flow', A. Darvas, R. Haehnle and D. Sands, Security in Pervasive Computing, 2005

Declassification Example

Declassification example from the paper, Fig. 6

Termination Example

Termination leak example from the paper, Fig. 8 (left)

Joana Fig. 1 top left

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 1, top left.

Joana Fig. 2 bottom left

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 2, bottom left.

Joana Fig. 2 top

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 2, top.

Joana Fig. 3 bottom left

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 3, bottom left.

Joana Fig. 3 bottom right

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 3, bottom right.

Joana Fig. 3 top left

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 3, top left.

Joana Fig. 3 top right

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 3, top right.

Joana Fig 13 left

Example from 'A new algorithm for low-deterministic security', D. Giffhorn and G. Snelting, International Journal of Information Security, 2015. Figure 13, left.

Example from 'A Hybrid Approach for Proving Noninterference of Java Programs', R. Kuesters, T. Truderung, B. Beckert, D. Bruns, M. Kirsten, and M. Mohr, 2015 IEEE 28th Computer Security Foundations Symposium.

Product

Example from 'Relational Verification using Product Programs', G. Barthe, J. M. Crespo, and C. Kunz, FM 2011

Smith

Example from 'Principles of Secure Information Flow Analysis', G. Smith, Malware Detection, 2007

Terauchi Fig. 1

Example from 'Secure Information Flow as a Safety Problem', T. Terauchi and A. Aiken, SAS 2005, Fig. 1

Terauchi Fig. 2

Example from 'Secure Information Flow as a Safety Problem', T. Terauchi and A. Aiken, SAS 2005, Fig. 2

Terauchi Fig. 3

Example from 'Secure Information Flow as a Safety Problem', T. Terauchi and A. Aiken, SAS 2005, Fig. 3

Comparators: P1

Examples for proving the first hyperproperty of comparators (sgn(compare(x,y)) = -sgn(compare(y,x)), a 2-hypersafety property), using general relational specifications. Example programs are taken from Sousa and Dillig, 'Cartesian Hoare Logic for Verifying k-Safety Properties', PLDI 2016 (https://github.com/marcelosousa/descartes/tree/master/benchmarks/pldi-16/stackoverflow).

ArrayInt_false

ArrayInt, incorrect version

ArrayInt_true

ArrayInt, correct version

CatBPos_false

CatBPos, incorrect version

Chromosome_false

Chromosome, incorrect version

Chromosome_true

Chromosome, correct version

CollItem_false

CollItem, incorrect version

CollItem_true

CollItem, correct version

Contact_false

Contact, incorrect version

Container_false_v1

ArrayInt, incorrect, first version

Container_false_v2

ArrayInt, incorrect, second version

Container_true

ArrayInt, correct version

DataPoint_false

DataPoint, incorrect version

FileItem_false

FileItem, incorrect version

FileItem_true

FileItem, correct version

Match_false

Match, incorrect version

Match_true

Match, correct version

NameComparator_false

NameComparator, incorrect version

NameComparator_true

NameComparator, correct version

Node_false

Node, incorrect version

Node_true

Node, correct version

NzbFile_false

NzbFile, incorrect version

NzbFile_true

NzbFile, correct version

PokerHand_false

PokerHand, incorrect version

PokerHand_true

PokerHand, correct version

Solution_false

Solution, incorrect version

Solution_true

Solution, correct version

TextPosition_false

TextPosition, incorrect version

TextPosition_true

TextPosition, correct version

Time_false

Time, incorrect version

Time_true

Time, correct version

Word_false

Word, incorrect version

Word_true

Word, correct version

Comparators: P2

Examples for proving the second hyperproperty of comparators (compare(x, y) > 0 && compare(y, z) > 0 ==> compare(x, z) > 0, a 3-hypersafety property), using general relational specifications.

Comparators: P3

Examples for proving the third hyperproperty of comparators (compare(x,y) = 0 ==> sgn(compare(x, z)) = sgn(compare(y, z)), a 3-hypersafety property), using general relational specifications.