No.063 Semantics and Verification of Object-Oriented Languages

Separation logic (SL) has gained widespread popularity as a formal foundation of tools that analyze and verify heap-manipulating programs. Its great asset lies in its assertion language, which can succinctly express how data structures are laid out in memory, and its discipline of local reasoning, which mimics human intuition about how to prove heap programs correct.

While the succinctness of separation logic makes it attractive for developers of program analysis tools, it also poses a challenge to automation: separation logic is a nonclassical logic that requires specialized theorem provers for discharging the generated proof obligations. SL-based tools therefore implement their own tailor-made theorem provers for this task. However, these theorem provers are not robust under extensions, e.g., involving reasoning about the data stored in heap structures.

I will present an approach that enables complete combinations of decidable separation logic fragments with other theories in an elegant way. The approach works by reducing SL assertions to first-order logic. The target of this reduction is a decidable fragment of first-order logic that fits well into the SMT framework. That is, reasoning in separation logic is handled entirely by an SMT solver. We have implemented our approach in the GRASShopper tool and used it successfully to verify interesting data structures.

Slides

Malware is a serious problem on mobile devices. The vision of this session’s speakers was a verified app store in which each application has been formally proven to be free of (certain) defects and exploits. They have built such a system and successfully applied it to dozens of challenge applications created by hostile red teams. The session describes their type system for information flow along with support for implicit invocation (intents and reflection), varieties of polymorphism, and other challenges that have arisen. Based on my CCS 2014 and ASE 2015 papers.

Slides