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 really clean, and it is likely to contain bugs and not being really user-friendly.

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.

If you can not visualize the video above, it may be due to security settings. The video files are stored on the MSR-INRIA lab servers and not on this server. You may modify your Flash security settings using the Adobe Flash Player Settings Manager or see the video on the MSR-INRIA CFlow webpage.

Other video formats (hosted on the MSR-INRIA CFlow webpage):

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

Download

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

License

CFlow is copyrighted "Copyright (C) 2009 The Microsoft Research-INRIA Joint Centre". It is distributed under the terms of the CeCILL-B license (a BSD-like license written in a French legal style).

Bibliography

@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 = "Fournet, C\'{e}dric and Rezk, Tamara",
  • title = "{C}ryptographically {S}ound {I}mplementations for {T}yped {I}nformation-{F}low {S}ecurity",
  • booktitle = "{ACM} {SIGPLAN-SIGACT} symposium on {P}rinciples {O}f {P}rogramming {L}anguages",
  • 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.

Valid XHTML 1.1

Valid CSS 2