Report title: Deductive Abstract Verification with Phi Types

Report time: May 25th, 13:30-15:00

Offline report location: B1002, Science Building

Host: Professor Zhang Min

Abstract:

The complexity and low level of detail of software often require that together with reasoning logics we use additional techniques to simplify the verification. One of the most well known techniques is refinement between layers of specifications where the desired properties are verified on abstract specifications down to concrete implementations. This technique has been successfully applied on several system such as the SEL4 micro-kernel verification, Compcert, and CertiKOS, among others. 

Despite of the good results obtained by refinement between layers of specification, abstraction layers must be constructed manually, and it is necessary to construct and apply additional verification artefacts to show that properties are applied among layers. Moreover, the gap between the implementation and the highest level of abstraction is often too large to apply one level of refinement and it is necessary to apply different abstractions. As a consequence the verification effort is too big and it becomes necessary to obtain more efficient techniques.

In this talk I introduce phi-types together with phi-SL, a novel separation-based logic that allows to verify directly low level implementations while reasoning on abstract levels without having to construct additional specification layers. Phi-types embed the abstraction on hoare-triplets and introduces a consequence rule that allows to shift between different abstractions. We implement phi-types and phi-SL in Isabelle/HOL together with a layer of automation that allows the verification of complex systems with relatively low effort. Using phi-systems we have verified a large portion of the Uniswap protocol for smart-contracts. Uniswap encodes in Solidity a very complex financial model resulting in a very challenging verification, which we successfully carry out in our framework with very good automation.

Introduction of Lectuer:

Dr. David Sanan is an Assistant Professor at the Singapore Institute of Technology. He received his M.S. degree in computer science and his PhD degree in Software Engineering and Artificial Intelligence from the University of Malaga, Malaga, Spain, in 2003 and 2009, respectively. His research interest covers formal methods applied to a wide number of applications going from programming language semantics to software verification. In particular, David has been working during the last years on applying formal methods to real-world applications like quantum computing, certification of smart contracts, and the verification of security micro-kernels in the Aerospace and Electric-Vehicle domain.