October 23, 2020
Abstract
We like code to be modular. That is, we want to be able to swap different pieces of implementation in and out as we build our software. This usually leads to sections of code that we entrust to do some job, but whose actual implementation is unknown to us or will otherwise be determined later. A common example is an API call that will eventually be linked to one of many possible implementations, requiring us to reason about client code not by inspecting some concrete API implementation but rather by assuming the API behavior will meet some specification. This complicates reasoning about client programs, as we must now account for the complete set of behaviors permitted by a specification.
This is particularly true when verifying relational properties that involve several programs, which can require specifications relating the behavior of implementation gaps across multiple executions. Does replacing one API with another refine a client’s behavior? Does some three-way code merge maintain the semantics of the original diffs? Does some procedure fail to leak sensitive data no matter what secret inputs it is provided? This talk will present the current state of our work on RHLE, a relational program logic designed for reasoning about multiple executions of programs with specified functions.