Paper 2012/205
Information-flow control for programming on encrypted data
J. C. Mitchell, R. Sharma, D. Stefan, and J. Zimmerman
Abstract
Using homomorphic encryption and secure multiparty computation, cloud servers may perform regularly structured computation on encrypted data, without access to decryption keys. However, prior approaches for programming on encrypted data involve restrictive models such as boolean circuits, or standard languages that do not guarantee secure execution of all expressible programs. We present an expressive core language for secure cloud computing, with primitive types, conditionals, standard functional features, mutable state, and a secrecy preserving form of general recursion. This language, which uses an augmented information-flow type system to prevent control-flow leakage, allows programs to be developed and tested using conventional means, then exported to a variety of secure cloud execution platforms, dramatically reducing the amount of specialized knowledge needed to write secure code. We present a Haskell-based implementation and prove that cloud implementations based on secret sharing, homomorphic encryption, or other alternatives satisfying our general definition meet precise security requirements.
Note: This document is the extended version of a CSF 2012 publication.
Metadata
- Available format(s)
-
PDF
- Category
- Foundations
- Publication info
- Published elsewhere. Unknown where it was published
- Keywords
- domain-specific languagessecure cloud computinginformation flow controlhomomorphic encryptionmultiparty computation
- Contact author(s)
- deian @ cs stanford edu
- History
- 2012-04-15: received
- Short URL
- https://ia.cr/2012/205
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2012/205,
author = {J. C. Mitchell and R. Sharma and D. Stefan and J. Zimmerman},
title = {Information-flow control for programming on encrypted data},
howpublished = {Cryptology {ePrint} Archive, Paper 2012/205},
year = {2012},
url = {https://eprint.iacr.org/2012/205}
}
