Approximate Reasoning for Markov Processes

Radu Mardare and Prakash Panangaden

We develop a fusion of logical and metrical principles for reasoning about Markov processes. More precisely, we lift metrics from processes to sets of processes satisfying a logical formula and explore how the satisfaction relation behaves as sequences of processes and sequences of formulas approach limits. A key new concept is dynamically-continuous metric bisimulation which is a property of (pseudo)metrics. We prove theorems about satisfaction in the limit, robustness theorems as well as giving a topological characterization of various classes of formulas. This work is aimed at providing approximate reasoning principles for Markov processes.

Monad-based Partial Correctness Assertions

Sergey Goncharov and Lutz Schröder

While the idea of encapsulating computational effects by monads has been eagerly adapted and developed in considerable detail for purposes of programming and denotational semantics, the realm of monad-based program logics still offers a lot of opportunities for further research and refinement of the existing ideas. In our recent and ongoing work we focus on the specific case of Hoare logic. We base our development on the crucial idea of identification of assertions as a certain kind of (relatively) well-behaved programs called innocent. This led us to a generic notion of a Hoare triple and a relative completeness result in the style of Cook. A reasonably mild and well-motivated assumption forming the cornerstone of our framework is the assumption of order-enrichment for the monad serving two purposes: providing semantics of iteration for programs in a domain-theoretic fashion and providing semantics of logical operations for assertions, such as disjunction, quantifiers and fixed points. While the truth value object is generated canonically in our framework, it turned out that it in general can be guaranteed to support full first order intuitionistic logic only over Sets. In such an instructive case as the local state monad, which lives in a category of presheaves, this is still true but nontrivial, as are several other details of instantiation of our generic framework to this particular case. Here we propose an extended treatment of the local state monad example.

Read paper

Towards Verified Shared-memory Cooperation for C

Lennart Beringer, Gordon Stewart, Robert Dockins and Andrew W. Appel

We report on the ongoing design of a novel architecture for verified separate compilation of C programs, in the context of the CompCert certified C compiler.

Read paper

Low-Level Program Verification using Matching Logic Reachability

Dwight Guth, Andrei Stefanescu and Grigore Rosu

Matching logic reachability is an emerging verification approach which uses a language-independent proof system to prove program properties based on the operational semantics. In this paper we apply this approach in the context of a low-level real-time language with interrupts, in which each instruction takes a specified time to execute. In particular, we verify that if the interrupts are scheduled with large enough intervals, the program execution terminates yielding the correct result. Surprisingly, it turns out that matching logic reachability can handle the low-level and real-time features of the language just by using their operational semantics, and that language specific reasoning is unnecessary.

Read paper

Memory Trace Oblivious Program Execution

Chang Liu, Michael Hicks and Elaine Shi

Cloud computing allows users to delegate data and computation to cloud service providers, at the cost of giving up physical control of their computing infrastructure. An attacker (e.g., insider) with physical access to the computing platform can perform various physical attacks, including probing memory buses and cold-boot style attacks. Previous work on secure (co-)processors provides hardware support for memory encryption and prevents direct leakage of sensitive data over the memory bus. However, an adversary snooping on the bus can still infer sensitive information from the memory access traces. Existing work on Oblivious RAM (ORAM) provides a solution for users to put all data in an ORAM; and accesses to an ORAM are obfuscated such that no information leaks through memory access traces. This method, however, incurs significant memory access overhead.

This work is the first to leverage programming language techniques to offer efficient memory-trace oblivious program execution, while providing formal security guarantees. We formally define the notion of memory-trace obliviousness, and provide a type system for verifying that a program satisfies this property. We also describe a compiler that transforms a program into a structurally similar one that satisfies memory trace obliviousness. To achieve optimal efficiency, our compiler partitions variables into several small ORAM banks rather than one large one, without risking security. We use several example programs to demonstrate the efficiency gains our compiler achieves in comparison with the naive method of placing all variables in the same ORAM.