Oblivious algebraic data types

Secure computation allows multiple parties to compute joint functions over private data without leaking any sensitive data, typically using powerful cryptographic techniques. Writing secure applications using these techniques directly can be challenging, resulting in the development of several programming languages and compilers that aim to make secure computation accessible. Unfortunately, many of these languages either lack or have limited support for rich recursive data structures, like trees. In this paper, we propose a novel representation of structured data types, which we call oblivious algebraic data types, and a language for writing secure computations using them. This language combines dependent types with constructs for oblivious computation, and provides a security-type system which ensures that adversaries can learn nothing more than the result of a computation. Using this language, authors can write a single function over private data, and then easily build an equivalent secure computation according to a desired public view of their data.

Preliminaries

Recursion, or the capacity of ‘self-reference’, has played a central role within mathematical approaches to understanding the nature of computation, from the general recursive functions of Alonzo Church to the partial recursive functions of Stephen C. Kleene and the production systems of Emil Post. Recursion has also played a significant role in the analysis and running of certain computational processes within computer science (viz., those with self-calls and deferred operations). Yet the relationship between the mathematical and computer versions of recursion is subtle and intricate. A recursively specified algorithm, for example, may well proceed iteratively if time and space constraints permit; but the nature of specific data structures—viz., recursive data structures—will also return a recursive solution as the most optimal process. In other words, the correspondence between recursive structures and recursive processes is not automatic; it needs to be demonstrated on a case-by-case basis.

Loop Extended Symbolic Execution on List Manipulating Programs

Current symbolic execution is challenged by its ability to deal with loops. The case gets worse for loops manipulating recursive data structures. In this paper, we extend classic symbolic execution techniques for error detection of programs manipulating lists in loops. The idea is to enhance the symbolic execution with the utilization of quantitative aspect of the shape, and to construct the exit state of the loop. The exit state is constrained by a set of numeric constraints containing normal symbolic variables in programs and instrumented symbolic variables on the shapes. A prototype tool has been implemented and experiments are conducted on some commonly used list manipulating programs.