Sciweavers

Share
CCS
2009
ACM

A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms

9 years 3 months ago
A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms
We enforce information flow policies in programs that run at multiple locations, with diverse levels of security. We build a compiler from a small imperative language with locality and security annotations down to distributed code linked to concrete cryptographic libraries. Our compiler splits source programs into local threads; inserts checks on auxiliary variables to enforce the source control flow; implements shared distributed variables using instead a series of local replicas with explicit updates; and finally selects cryptographic mechanisms for securing the communication of updates between locations. We establish computational soundness for our compiler: under standard assumptions on cryptographic primitives, all confidentiality and integrity properties of the source program also hold with its distributed code, despite the presence of active adversaries that control all communications and some of the program locations. We also present performance results for the code obtain...
Cédric Fournet, Gurvan Le Guernic, Tamara R
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where CCS
Authors Cédric Fournet, Gurvan Le Guernic, Tamara Rezk
Comments (0)
books