International Association
for Cryptologic Research

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.