Secure Distributed Computations and their Proofs

Cryptographic Implementations of Information-Flow Security

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues.

We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract information-flow policy for accessing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing.

We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a cryptographic type system for a target probabilistic language. Our typing rules enforce the correct usage of cryptographic primitives against active adversaries; from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We show type soundness for a variant of the non-interference property, then show that our translation preserves typability.

We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.

Prototype

The theory has been implemented in a prototype called "CFlow". It has been coded in F#, developed mainly on Linux using mono (as a substitute to .NET), and partially tested under Windows (relying on .NET and Cygwin). It is only a prototype realized in order to test our theory and ideas. As a consequence, its code is not as clean as could be desired, and is likely to contain bugs. The code is distributed under the terms of the CeCILL-B license.

CFlow is distributed under 2 forms:

  • cflow contains only an executable version of the pre-compiler dwl2cml.exe, the libraries needed to compile the code generated by dwl2cml.exe, and some example DWL files.
  • cflow-src contains all the source code of CFlow.

In order to execute our pre-compiler (dwl2cml.exe) and then compile the code returned, a few programs are needed in addition to CFlow.

  • A Microsoft .NET framework (for example, .NET (at least 2.0 ?) under Windows, and Mono under Linux) is all that is needed to run dwl2cml.exe.
  • To compile the generated code, F# (version 1.9.7.8 or higher ... maybe) is required. In order to use the provided Makefile, in addition to 'make' of course, Cygwin is highly recommended under Windows.
  • To compile CFlow from sources and use additional features, GraphViz and ps2eps (itself requiring Perl and Ghostscript which usually are installed by default on Linux and Cygwin) are required. Additionally, fixbb.pl and rotateEps.pl are needed in the same directory as the Makefile in order to build dwl2cml execution reports.

To execute the pre-compiler, type: [mono] dwl2cml[.exe] file.dwl
For (little) usage information: [mono] dwl2cml[.exe] --help

Demo / Tutorial

The following is a demonstration of the compiler in action. The demo starts by coding a simple unsecured chat program. An integrity attack and a confidentiality attack are then performed against the generated program. The code is modified to protect the integrity and confidentiality of messages, and the attacks are replayed. Finally, a quick view of the generated code is given.

Other video formats:

You can see a shorter version of the demo on YouTube or Dailymotion.

Bibliography

Draft full FHE paper: Information-Flow Types for Homomorphic Encryption, Cédric Fournet and Jérémy Planul, Tamara Rezk May 2011. With typechecker prototype. 

@inproceedings{tpm-esop11,
  author    = {C{\'e}dric Fournet and
               J{\'e}r{\'e}my Planul},
  title     = {{C}ompiling {I}nformation-{F}low {S}ecurity to {M}inimal {T}rusted {C}omputing
               {B}ases},
  booktitle = "20th {E}uropean {S}ymposium on {P}rogramming ({ESOP}'11)",
  year      = 2011,
  month     = mar,
  isbn      = {978-3-642-19717-8},
  pages     = {216-235},
  location  = {Saarbr{\"u}cken, Germany},
  ee        = {http://dx.doi.org/10.1007/978-3-642-19718-5_12},
  publisher = {Springer},
}

ESOP paper: Compiling Information-Flow Security to Minimal Trusted Computing Bases, Cédric Fournet and Jérémy Planul, 2011.

Draft full paper: Compiling Information-Flow Security to Minimal Trusted Computing Bases, Cédric Fournet and Jérémy Planul, July 2010. With sample files. 

@inproceedings{cflow-ccs09,
  author = "Fournet, C\'{e}dric and Le Guernic, Gurvan and Rezk, Tamara",
  title = "{A} {S}ecurity-{P}reserving {C}ompiler for {D}istributed {P}rograms: {F}rom {I}nformation-{F}low {P}olicies to {C}ryptographic {M}echanisms",
  booktitle = "{ACM} conference on {C}omputer and {C}ommunications {S}ecurity",
  year = 2009,
  month = nov,
  isbn = {978-1-60558-894-0},
  pages = {432--441},
  location = {Chicago, Illinois, USA},
  doi = {http://doi.acm.org/10.1145/1653662.1653715},
  publisher = {ACM},
  address = {New York, NY, USA},
}

CCS paper: A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms, Cédric Fournet, Gurvan Le Guernic and Tamara Rezk, 2009. 

@inproceedings{cflow-popl08,
  author    = {C\'edric Fournet and Tamara Rezk},
  title     = {Cryptographically Sound Implementations for Typed Information-Flow Security},
  booktitle = "35th Annual ACM SIGPLAN-SIGACT Symposium on Principles
  of Programming Languages (POPL'08)",
  month = jan,
  year = 2008,
  publisher = {ACM Press},
  address = {San Francisco, USA}
  pages = {323--335}
}

POPL paper: Cryptographically Sound Implementations for Typed Information-Flow Security, Cédric Fournet and Tamara Rezk, 2007.

Draft full paper: Cryptographically Sound Implementations for Typed Information-Flow Security, Cédric Fournet and Tamara Rezk, May 2009.