pith. sign in

arxiv: 1907.01727 · v1 · pith:U3X634QCnew · submitted 2019-07-03 · 💻 cs.CR · cs.PL

Uncovering Information Flow Policy Violations in C Programs

Darion Cassel , Yan Huang , Limin Jia This is my paper

Pith reviewed 2026-05-25 10:37 UTC · model grok-4.3

classification 💻 cs.CR cs.PL
keywords information flowC programspolicy violationstype systemnoninterferencecryptographic applicationssource-to-source translationsecurity policies
0
0 comments X

The pith

A source-to-source translation embeds information flow policies into C types so existing compilers can detect violations with a noninterference proof.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a way to specify secrecy, integrity, and sequencing policies for C programs, especially in cryptographic code. Annotations for these policies are turned into ordinary C types through a translation step, letting standard compilers perform the checks instead of requiring new analysis engines. Case studies on real libraries show the approach scales to large bodies of code and catches subtle errors such as improper data flows or protocol ordering. Formal connections are established to an information flow type system, along with a proof that the method guarantees noninterference. A reader would care because the technique offers a lighter, compiler-based alternative for enforcing security policies without sacrificing formal backing.

Core claim

We embed the policy annotations in C's type system via a source-to-source translation and leverage existing C compilers to check for policy violations, achieving high performance and scalability. We show formal connections between the policy annotations and an information flow type system and prove a noninterference guarantee. Case studies of recent cryptographic libraries demonstrate that the method can express detailed policies for large C codebases and uncover subtle violations.

What carries the argument

Source-to-source translation that encodes policy annotations directly as C types for enforcement by standard compilers.

If this is right

  • Cryptographic C codebases can be checked for secrecy and integrity violations using only unmodified compilers.
  • Subtle errors such as sending private data over public channels become detectable at compile time.
  • Sequencing constraints on protocol steps can be enforced through the same type-based mechanism.
  • The approach applies to large existing libraries without requiring custom static-analysis infrastructure.
  • A noninterference guarantee holds for any program that type-checks under the translated policies.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same translation pattern might be adapted to other languages whose type systems can encode similar flow constraints.
  • Security teams could integrate policy checking into ordinary build pipelines rather than maintaining separate verification suites.
  • The formal link to noninterference opens the possibility of composing this method with other information-flow analyses.
  • If the translation is shown sound for additional policy classes, the technique could cover ordering and integrity rules beyond the original case studies.

Load-bearing premise

The source-to-source translation correctly and completely encodes the intended information flow policies into C types without introducing false negatives or positives.

What would settle it

A C program that violates an information flow policy but produces no compiler error after translation, or a policy-compliant program that the translated types incorrectly reject.

Figures

Figures reproduced from arXiv: 1907.01727 by Darion Cassel, Limin Jia, Yan Huang.

Figure 1
Figure 1. Figure 1: Overview of FlowNotation and connections to the formal model. 3 [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Syntax of polC The encodeA function, as before, requires the argument to have the AlicePriv secrecy label. In addition, the return value from encodeA will have the integrity label EncodedBal, stating that it is endorsed by the encodeA function to be properly encoded. The yao execA function requires the argument to have the same integrity label. If only programmer-approved encoding functions are annotated w… view at source ↗
Figure 3
Figure 3. Figure 3: Typing rules The subtyping relation s1 ≤ s2 is standard: most types are covariant except function argument types, which are contravariant, and pointer content types, which are invariant. ρBt denotes ρ guards t. It is defined as ρ v labOf (t). Here labOf (t) is the outermost label of type t; for instance, ⊥ B int (AlicePrivate, ⊥I ), (AlicePrivate, ⊥I ) B int (AlicePrivate, ⊥I ). Finally s t ρ is the type r… view at source ↗
Figure 4
Figure 4. Figure 4: Mapping annotations to types Da; Fa; Γa ` hhvii ⇒ lv tpOf (lv) = T ρ Da(T) = (struct T{β1, · · · , βn}) ∀i ∈ [1, n], ρ = labOf (hhβiii) Da; Fa; Γa;t ` hhv.iii ⇒ lv.i L-Field-U Da; Fa; Γa ` hhvii ⇒ lv tpOf (lv) = T ρ Da(T) = (struct T{β1, · · · , βn}) ∃i ∈ [1, n], ρ 6= labOf (hhβiii) Da; Fa; Γa;t ` hhv.iii ⇒ let y : T ⊥ = reLab(⊥ ⇐ ρ) lv in (y@T ⊥).i L-Field Da; Fa; Γa ` hhvii ⇒ lv tpOf (lv) = b ρ Da; Fa; Γ… view at source ↗
Figure 5
Figure 5. Figure 5: Mapping of expressions types, depending on the context under which they are used: n@int U and n@int ρ are translated into different terms. A value is mapped to itself with its type annotated. For example, integers are given int U type, since they are unlabeled. Da; Fa; Γa ` hhnii ⇒ n@int U V-L-Int Expression mapping rules are listed in [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Type translation However, this involves label operations, which µC’s type system cannot handle. L-deref and L-assign are similar. The mapping of if statements (L-If) relabels the conditional v1 to have int ⊥ type, so the branches are typed under the same program counter as the if expression. We write reLab(⊥ ⇐ ρ) as a short hand for a sequence of relabeling operations reLab(` :: ⊥ ⇐ `n::>)· · ·reLab(`i ::⊥… view at source ↗
Figure 7
Figure 7. Figure 7: Expression translation 4.3 Correctness We prove a correctness theorem, which states that if our translated nominal type system declares an expres￾sion e well-typed, then the labeled expression el , where e is translated from, is well-typed under polC ’s type system. Formally: Theorem 2 (Translation Soundness (Typing)). If Da; Fa; Γa; s ` hheii = le, hhDaii = Dl, hhFaii = Fl, hhΓaii = Γl, JDlK = D, JΓlKD = … view at source ↗
Figure 8
Figure 8. Figure 8: Evaluation Results. Sec, Int, and Seq are the number of secrecy, integrity, and sequencing policies. [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Processing Time vs Number of Annotations and Time Per Processing Stage [PITH_FULL_IMAGE:figures/full_fig_p023_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Operational Semantics of Extended polC Case: E ends in P-E-Deref By assumption 33 [PITH_FULL_IMAGE:figures/full_fig_p033_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Typing Rules for Values in Extended polC B.5 Summary of Typing Rules for Paired polC First we define subtyping relations and policy operations below. S1 vS S2 I1 vI I2 (S1, I1) v (S2, I2) ⊥ v ρ ρ v > `1 v `2 ρ1 v ρ2 `1 :: ρ1 v `2 :: ρ2 ρ1 t ρ2 = ρ2 t ρ1 ρ t ⊥ = ρ ρ t > = > ` = `1 t `2 ρ = ρ1 t ρ2 `1 :: ρ1 t `2 :: ρ2 = ` :: ρ b ≤ b 0 t ≤ t 0 s ≤ s 0 b ≤ b ≤Refl b ≤ b 0 b 0 ≤ b 00 b ≤ b 00 ≤Trans unit ≤ uni… view at source ↗
Figure 12
Figure 12. Figure 12: Typing Rules for Expressions in Extended [PITH_FULL_IMAGE:figures/full_fig_p040_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Translation Rules Lemma 33. If β does not include ⊥, then noBot(hhβii). Proof (sketch): By induction over the structure of β. The translation rules does not insert ⊥ except for functions. Lemma 34 (Value Translation Soundness). If E :: Da; Fa; Γa ` hhvii = lv , tpOf (lv) = s, hhDaii = Dl, hhFaii = Fl, hhΓaii = Γl, JDlK = D, JΓlKD = (Γ, D1), JFlKD = (F, D2), JlvKD = (v 0 , D3), and D ∪ D1 ∪ D2 ∪ D3; F; ·; … view at source ↗
Figure 14
Figure 14. Figure 14: Translation Rules (1) Da; Fa; Γa ` hhnii ⇒ n@int U By examining the translation rules, only T-Int applies (2) Jn@int U KD = (n, ·), By typing rules (3) D ∪ D1 ∪ D2; F; ·; Γ ` n : int By typing rule V-Int (4) Dl ; Fl ; ·; Γl ` n : int U By type translation (5) Jint U KD = (int, ) Case: E ends in V-L-Var rule. By assumption: (1) Da; Fa; Γa ` hhxii ⇒ x@hhβii and Γa(x) = β By examining the translation rules, … view at source ↗
read the original abstract

Programmers of cryptographic applications written in C need to avoid common mistakes such as sending private data over public channels, modifying trusted data with untrusted functions, or improperly ordering protocol steps. These secrecy, integrity, and sequencing policies can be cumbersome to check with existing general-purpose tools. We have developed a novel means of specifying and uncovering violations of these policies that allows for a much lighter-weight approach than previous tools. We embed the policy annotations in C's type system via a source-to-source translation and leverage existing C compilers to check for policy violations, achieving high performance and scalability. We show through case studies of recent cryptographic libraries and applications that our work is able to express detailed policies for large bodies of C code and can find subtle policy violations. To gain formal understanding of our policy annotations, we show formal connections between the policy annotations and an information flow type system and prove a noninterference guarantee.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents a source-to-source translation technique that embeds secrecy, integrity, and sequencing policy annotations into C types so that standard C compilers can detect violations. It reports case studies on cryptographic libraries and applications, demonstrates formal connections between the annotations and an existing information flow type system, and proves a noninterference guarantee.

Significance. If the translation is sound, the method supplies a lightweight, high-performance alternative to specialized information-flow tools for C, which is valuable for cryptographic code. The explicit formal connection to an information-flow type system and the noninterference proof are strengths that distinguish the work from purely heuristic approaches.

major comments (2)
  1. [§4] §4 (Translation soundness): The claim that the source-to-source translation faithfully encodes policies for all C constructs (pointer arithmetic, unions, function pointers, variadic functions) is load-bearing for both the compiler-based checking guarantee and the noninterference result, yet the manuscript provides only high-level sketches rather than a complete case analysis or reduction to the underlying C semantics.
  2. [§5] §5 (Noninterference proof): The proof relies on the translation preserving the information-flow type system’s judgments, but no explicit statement is given of the conditions under which the embedding is faithful (e.g., absence of implementation-defined behavior or undefined behavior that could bypass labels).
minor comments (2)
  1. The abstract and introduction use “sequencing policies” without a precise definition until later sections; a forward reference or early definition would improve readability.
  2. Figure 2 (example translation) would benefit from an accompanying table that lists each policy construct and its C-type encoding.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the importance of explicit soundness arguments for the translation and the noninterference result. Both points are well-taken; we address them below and will strengthen the formal sections accordingly.

read point-by-point responses

  1. Referee: [§4] §4 (Translation soundness): The claim that the source-to-source translation faithfully encodes policies for all C constructs (pointer arithmetic, unions, function pointers, variadic functions) is load-bearing for both the compiler-based checking guarantee and the noninterference result, yet the manuscript provides only high-level sketches rather than a complete case analysis or reduction to the underlying C semantics.

    Authors: We agree that the current presentation of §4 relies on high-level sketches for the more intricate C constructs. In the revised manuscript we will expand §4 with an explicit case-by-case analysis for pointer arithmetic, unions, function pointers, and variadic functions, each accompanied by a brief reduction to the relevant clauses of the C standard semantics. This will make the load-bearing claim fully supported and will also clarify the scope of the compiler-based checking guarantee. revision: yes

  2. Referee: [§5] §5 (Noninterference proof): The proof relies on the translation preserving the information-flow type system’s judgments, but no explicit statement is given of the conditions under which the embedding is faithful (e.g., absence of implementation-defined behavior or undefined behavior that could bypass labels).

    Authors: We concur that the faithfulness conditions should be stated explicitly rather than left implicit. The revised §5 will include a dedicated paragraph (or short subsection) enumerating the assumptions under which the embedding preserves judgments—most importantly, the absence of undefined behavior or implementation-defined behavior that could circumvent the inserted labels. We will also note that the noninterference theorem is stated relative to those assumptions, consistent with the standard practice for information-flow results on real languages. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation is self-contained via explicit translation and proof

full rationale

The paper defines a source-to-source translation that embeds policy annotations directly into C types, then uses standard compilers for checking. It separately establishes formal connections to an information flow type system and proves noninterference as part of the presented work. No quoted step reduces a claimed prediction or result to a fitted parameter, self-referential definition, or unverified self-citation chain; the central claims rest on the translation definition and the proof rather than on prior outputs of the same authors.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the assumption that the translation step faithfully represents the policies; no free parameters or invented entities are described in the abstract.

axioms (1)
  • domain assumption The source-to-source translation preserves the semantics of the original C program with respect to the information flow policies.
    Invoked to ensure that compiler checks correspond to actual policy violations.

pith-pipeline@v0.9.0 · 5677 in / 1080 out tokens · 30982 ms · 2026-05-25T10:37:53.672661+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

73 extracted references · 73 canonical work pages

  1. [1]

    https://github.com/krb5/krb5/tree/master/src/lib/krb5/asn.1,

    Kerberos ASN.1 Encoder. https://github.com/krb5/krb5/tree/master/src/lib/krb5/asn.1,

    work page

  2. [2]

    Typestate-oriented program- ming

    Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestate-oriented program- ming. In Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Program- ming Systems Languages and Applications , OOPSLA ’09, 2009

    work page 2009

  3. [3]

    Jasmin: High-assurance and high-speed cryptography

    Jos´ e Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gr´ egoire, Vincent La- porte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. Jasmin: High-assurance and high-speed cryptography. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17, 2017

    work page 2017

  4. [4]

    Rajamani

    Thomas Ball and Sriram K. Rajamani. The slam project: Debugging system software via static anal- ysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’02, 2002

    work page 2002

  5. [5]

    Hybrid information flow analysis for real-world c code

    Gerg¨ o Barany and Julien Signoles. Hybrid information flow analysis for real-world c code. In Interna- tional Conference on Tests and Proofs . Springer, 2017

    work page 2017

  6. [6]

    Non-interactive oblivious transfer and applications

    Mihir Bellare and Silvio Micali. Non-interactive oblivious transfer and applications. In Proceedings on Advances in Cryptology, CRYPTO ’89, 1989

    work page 1989

  7. [7]

    pycparser

    Eli Bendersky. pycparser. https://github.com/eliben/pycparser, 2013. [Online]

    work page 2013

  8. [8]

    Refinement types for secure implementations

    Jesper Bengtson, Karthikeyan Bhargavan, C´ edric Fournet, Andrew D Gordon, and Sergio Maffeis. Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS), 2011

    work page 2011

  9. [9]

    End-to-end multilevel hybrid information flow control

    Lennart Beringer. End-to-end multilevel hybrid information flow control. In Asian Symposium on Programming Languages and Systems. Springer, 2012

    work page 2012

  10. [10]

    The software model checker blast

    Dirk Beyer, Thomas A Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker blast. International Journal on Software Tools for Technology Transfer , 2007

    work page 2007

  11. [11]

    Cpachecker: A tool for configurable software verification

    Dirk Beyer and M Erkan Keremoglu. Cpachecker: A tool for configurable software verification. In International Conference on Computer Aided Verification . 2011. 25

    work page 2011

  12. [12]

    Cryptographically ver- ified implementations for tls

    Karthikeyan Bhargavan, C´ edric Fournet, Ricardo Corin, and Eugen Zalinescu. Cryptographically ver- ified implementations for tls. In Proceedings of the 15th ACM conference on Computer and communi- cations security. ACM, 2008

    work page 2008

  13. [13]

    Karthikeyan Bhargavan, C´ edric Fournet, and Andrew D. Gordon. Modular verification of security protocol code by typing. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, 2010

    work page 2010

  14. [14]

    An efficient cryptographic protocol verifier based on prolog rules

    Bruno Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proceedings of the 14th IEEE Workshop on Computer Security Foundations , CSFW ’01, 2001

    work page 2001

  15. [15]

    Rustan M

    Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. Vale: Verifying high-performance cryptographic assembly code. In 26th USENIX Security Symposium (USENIX Security 17) , 2017

    work page 2017

  16. [16]

    Idris, a general-purpose dependently typed programming language: Design and imple- mentation

    Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and imple- mentation. Journal of Functional Programming, 2013

    work page 2013

  17. [17]

    Scrash: A system for generating secure crash infor- mation

    Pete Broadwell, Matt Harren, and Naveen Sastry. Scrash: A system for generating secure crash infor- mation. In Proceedings of the 12th Conference on USENIX Security Symposium - Volume 12, SSYM’03, 2003

    work page 2003

  18. [18]

    Paragon for practical programming with information-flow control

    Niklas Broberg, Bart Delft, and David Sands. Paragon for practical programming with information-flow control. In Proceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 8301, 2013

    work page 2013

  19. [19]

    Paralocks: Role-based information flow control and beyond

    Niklas Broberg and David Sands. Paralocks: Role-based information flow control and beyond. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, 2010

    work page 2010

  20. [20]

    Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs

    Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation , OSDI’08, 2008

    work page 2008

  21. [21]

    Semantic type qualifiers

    Brian Chin, Shane Markstrum, and Todd Millstein. Semantic type qualifiers. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation , PLDI ’05, 2005

    work page 2005

  22. [22]

    Chong and A

    S. Chong and A. C. Myers. End-to-end enforcement of erasure and declassification. In 2008 21st IEEE Computer Security Foundations Symposium , 2008

    work page 2008

  23. [23]

    A tool for checking ANSI-C programs

    Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004) , 2004

    work page 2004

  24. [24]

    Computationally sound, automated proofs for security pro- tocols

    V´ eronique Cortier and Bogdan Warinschi. Computationally sound, automated proofs for security pro- tocols. In European Symposium on Programming. Springer, 2005

    work page 2005

  25. [25]

    End-to-end verification of information-flow security for c and assembly programs

    David Costanzo, Zhong Shao, and Ronghui Gu. End-to-end verification of information-flow security for c and assembly programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation , PLDI ’16, 2016

    work page 2016

  26. [26]

    The astr´ ee analyzer

    Patrick Cousot, Radhia Cousot, J´ erˆ ome Feret, Laurent Mauborgne, Antoine Min´ e, David Monniaux, and Xavier Rival. The astr´ ee analyzer. InEuropean Symposium on Programming. Springer, 2005. 26

    work page 2005

  27. [27]

    The scyther tool: Verification, falsification, and analysis of security protocols

    Cas JF Cremers. The scyther tool: Verification, falsification, and analysis of security protocols. In International Conference on Computer Aided Verification . Springer, 2008

    work page 2008

  28. [28]

    Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C. In Software Engineering and Formal Methods . Springer Berlin Heidelberg, 2012

    work page 2012

  29. [29]

    Fast Oblivious AES A Dedicated Application of the MiniMac Protocol

    Ivan Damg˚ ard and Rasmus Zakarias. Fast Oblivious AES A Dedicated Application of the MiniMac Protocol. In Progress in Cryptology – AFRICACRYPT 2016 . Springer International Publishing, 2016

    work page 2016

  30. [30]

    MiniAES Repository

    Ivan Damg˚ ard and Rasmus Zakarias. MiniAES Repository. https://github.com/AarhusCrypto/ MiniAES, 2016. [Online]

    work page 2016

  31. [31]

    Enforcing high-level protocols in low-level software

    Robert DeLine and Manuel F¨ ahndrich. Enforcing high-level protocols in low-level software. In Proceed- ings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation , PLDI ’01, 2001

    work page 2001

  32. [32]

    Absentminded Crypto Kit Repository

    Jack Doerner. Absentminded Crypto Kit Repository. https://bitbucket.org/jackdoerner/ absentminded-crypto-kit/, 2015. [Online]

    work page 2015

  33. [33]

    Scaling oram for secure computation

    Jack Doerner and Abhi Shelat. Scaling oram for secure computation. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security , CCS ’17, 2017

    work page 2017

  34. [34]

    Static detection of dynamic memory errors

    David Evans. Static detection of dynamic memory errors. In Proceedings of the ACM SIGPLAN 1996 Conference on Programming Language Design and Implementation , PLDI ’96, 1996

    work page 1996

  35. [35]

    Foster, Manuel F¨ ahndrich, and Alexander Aiken

    Jeffrey S. Foster, Manuel F¨ ahndrich, and Alexander Aiken. A theory of type qualifiers. In Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation , PLDI ’99, 1999

    work page 1999

  36. [36]

    Type qualifiers: lightweight specifications to improve soft- ware quality

    Jeffrey Scott Foster and Alexander S Aiken. Type qualifiers: lightweight specifications to improve soft- ware quality. PhD thesis, University of California, Berkeley, 2002

    work page 2002

  37. [37]

    The seahorn verification framework

    Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A Navas. The seahorn verification framework. In International Conference on Computer Aided Verification . 2015

    work page 2015

  38. [38]

    Myers, and Fred B Schneider

    Elisavet Kozyri, Owen Arden, Andrew C. Myers, and Fred B Schneider. JRIF: Reactive Information Flow Control for Java . Feb 2016

    work page 2016

  39. [39]

    Dafny: An automatic program verifier for functional correctness

    K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning . Springer, 2010

    work page 2010

  40. [40]

    J. R. Lewis and B. Martin. Cryptol: high assurance, retargetable crypto development and validation. In IEEE Military Communications Conference, 2003. MILCOM 2003. , 2003

    work page 2003

  41. [41]

    Aravind Machiry, Chad Spensky, Jake Corina, Nick Stephens, Christopher Kruegel, and Giovanni Vigna. Dr. checker: A soundy analysis for linux kernel drivers. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, 2017

    work page 2017

  42. [42]

    Pantaloons/RSA Repository

    Michael McGee. Pantaloons/RSA Repository. https://github.com/pantaloons/RSA/, 2011. [Online]

    work page 2011

  43. [43]

    Andrew C. Myers. Jflow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’99, 1999. 27

    work page 1999

  44. [44]

    Information flow inference for ml

    Fran¸ cois Pottier and Vincent Simonet. Information flow inference for ml. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’02, 2002

    work page 2002

  45. [45]

    Saarinen

    Markku-Juhani O. Saarinen. Tiny SHA3. https://github.com/mjosaarinen/tiny_sha3, 2016. [On- line]

    work page 2016

  46. [46]

    Sabelfeld and A

    A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 2003

    work page 2003

  47. [47]

    R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering , 1986

    work page 1986

  48. [48]

    Secure distributed programming with value-dependent types

    Nikhil Swamy, Juan Chen, C´ edric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011

    work page 2011

  49. [49]

    Vachharajani, M

    N. Vachharajani, M. J. Bridges, J. Chang, R. Rangan, G. Ottoni, J. A. Blome, G. A. Reis, M. Vach- harajani, and D. I. August. Rifle: An architectural framework for user-centric information-flow security. In 37th International Symposium on Microarchitecture (MICRO-37’04) , 2004

    work page 2004

  50. [50]

    A type-based approach to program security

    Dennis Volpano and Geoffrey Smith. A type-based approach to program security. In Michel Bidoit and Max Dauchet, editors, TAPSOFT ’97: Theory and Practice of Software Development . Springer Berlin Heidelberg, 1997

    work page 1997

  51. [51]

    A. C. C. Yao. How to generate and exchange secrets. In 27th Annual Symposium on Foundations of Computer Science (sfcs 1986) , 1986

    work page 1986

  52. [52]

    NIIBE Yutaka. gnuk. https://www.fsij.org/category/gnuk.html, 2018. [Online]

    work page 2018

  53. [53]

    Obliv-C: A Language for Extensible Data-Oblivious Computation

    S Zahur, D Evans IACR Cryptology ePrint Archive, and 2015. Obliv-C: A Language for Extensible Data-Oblivious Computation

    work page 2015

  54. [54]

    Zahur and D

    S. Zahur and D. Evans. Circuit structures for improving efficiency of security and privacy tools. In 2013 IEEE Symposium on Security and Privacy , 2013

    work page 2013

  55. [55]

    Obliv-C Repository

    Samee Zahur. Obliv-C Repository. https://github.com/samee/obliv-c/, 2015. [Online]

    work page 2015

  56. [56]

    SCDtoObliv Repository

    Samee Zahur and Darion Cassel. SCDtoObliv Repository. https://github.com/samee/obliv-c/ tree/obliv-c/SCDtoObliv, 2015. [Online]

    work page 2015

  57. [57]

    Using cqual for static analysis of authorization hook placement

    Xiaolan Zhang, Antony Edwards, and Trent Jaeger. Using cqual for static analysis of authorization hook placement. In USENIX Security Symposium, pages 33–48, 2002

    work page 2002

  58. [58]

    Pool Framework Documentation

    Ruiyu Zhu, Yan Huang, and Darion Cassel. Pool Framework Documentation. https://jimu-pool. github.io/PoolFramework/, 2017. [Online]

    work page 2017

  59. [59]

    Pool Framework Repository

    Ruiyu Zhu, Yan Huang, and Darion Cassel. Pool Framework Repository. https://github.com/ jimu-pool/PoolFramework/, 2017. [Online]

    work page 2017

  60. [60]

    Pool: Scalable on-demand secure computation service against malicious adversaries

    Ruiyu Zhu, Yan Huang, and Darion Cassel. Pool: Scalable on-demand secure computation service against malicious adversaries. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17, 2017. 28 A Summary of µC: A Core Calculus with Nominal Typing We summarize the syntax, operational semantics, and typing rules for µC ...

    work page 2017

  61. [61]

    x = σ2 and y =e+ 2 and σ2 /i e+ 2 is closed

    For i ∈ { 1, 2, •} if σ1 /i e+ 1 is closed and Ψ ⊢ σ1 /i e+ 1 − →x /i y then exists σ2 and e+ 2 s.t. x = σ2 and y =e+ 2 and σ2 /i e+ 2 is closed

    work page

  62. [62]

    x = σ2 and y =e2 and σ2 /i e2 is closed

    For i ∈ {1, 2} if σ1 /i e1 is closed and Ψ ⊢ σ1 /i e1 − →x /i y then exists σ2 and e2 s.t. x = σ2 and y =e2 and σ2 /i e2 is closed. Proof (sketch): By induction over the structure of the operational semantic rules. Lemma 7 (Distributivity of Projection for Expressions) . ⌊e+[x ⇐v+]⌋i = ⌊e+⌋i[x ⇐ ⌊v+⌋i] Proof. By induction over the structure of e+. Most ca...

    work page

  63. [63]

    40 Proof (sketch): By induction over the structure of E

    If E ::D;F ; Σ; Γ;pc ⊢e :s and Σ ≤ Σ′ then D;F ; Σ′; Γ;pc ⊢e :s. 40 Proof (sketch): By induction over the structure of E. We use Lemma 14 in cases where pc is used in the premises. Lemma 17 (Projection well-typed). If E ::D; Σ; Γ⊢v :s then ∀i ∈ {1, 2}, D; Σ; Γ⊢ ⌊v⌋i :s Proof (sketch): By induction over the structure of E. Lemma 18 (Substitution)

    work page

  64. [64]

    If E ::D;F ; Σ; Γ,x :s ⊢v′ :s′ and D; ;F ; Σ; Γ⊢v :s then D;F ; Σ; Γ⊢v′[x ⇐v] :s′

    work page

  65. [65]

    Lemma 19

    If E ::D;F ; Σ; Γ,x :s; pc ⊢e :s′ and D;F ; Σ; Γ⊢v :s then D;F ; Σ; Γ;pc ⊢e[x ⇐v] :s′ Proof (sketch): By induction over the structure of E. Lemma 19

    work page

  66. [66]

    If s ≤T ρ then s =T ρ′

    work page

  67. [67]

    If s ≤ ptr(s′) ρ then s = ptr(s′) ρ′

    work page

  68. [68]

    Proof (sketch): By induction over the derivation s ≤s′

    If s ≤ [pcf](t1 →t2)ρ then s = [pc′ f](t′ 1 →t′ 2)ρ′ and pcf ⊑ pc′ f , t1 ≤t′ 1 and t′ 2 ≤t2. Proof (sketch): By induction over the derivation s ≤s′. Lemma 20 (Inversion)

    work page

  69. [69]

    If D;F ; · ⊢ (T ){v1, · · ·,vn} :T ρ, then D(T ) = {s1, · · ·,s 2} and ∀i ∈ [1,n ], D;F ; · ⊢ vi :si

    work page

  70. [70]

    If D;F ; · ⊢ loc : ptr(s) ρ, loc ∈ dom(σ), and D;F ⊢σ : Σ, then D;F ; ·; pc ⊢σ(loc) :s

    work page

  71. [71]

    If D;F ; · ⊢ f : [pcf](t1 →t2)ρ, f(x) =e ∈ dom(Ψ) and D;F ⊢ Ψ, then D;F ;x :t1; pcf ⊢e :t2

    work page

  72. [72]

    ρ ⊿s and ρ ∈H

    If D;F ; · ⊢ ⟨v1 |v2⟩ :s then ∀i ∈ [1, 2], D;F ; · ⊢ vi :s and ∃ρ, s.t. ρ ⊿s and ρ ∈H. Proof (sketch): By induction over the typing derivation. Lemma 21 (Value is typed w/o PC). If E ::D;F ; Σ; Γ;pc ⊢v :s then D;F ; Σ; Γ⊢v :s. Proof (sketch): By induction over the structure of E. In the cases of E-Sub and E-Pair, we directly apply I.H. and then apply the ...

    work page

  73. [73]

    Proof (sketch): By induction over the typing derivation of the value

    If D;F ; Σ;·; ⊥ ⊢ v : int ρ, and ρ /∈H, then ⌊v⌋1 = ⌊v⌋2. Proof (sketch): By induction over the typing derivation of the value. Definition 29 (Equivalent substitution). We define D;F ⊢δ1 ≈H δ2 : Γ iff for all x ∈ dom(Γ), D;F ; ·; ·; ⊢ δi(x) : Γ(x) (i ∈ {1, 2}) and δ1(x) =δ2(x) if labOf (Γ(x)) /∈H. Γ ⊢δ1 ⊿◁δ2 =δ Γ ⊢ · ⊿◁ · = · Γ ⊢δ1 ⊿◁δ2 =δ labOf (Γ(x)) ∈H Γ ...

    work page