Modular Specification and Verification of Security Properties for Mainstream Languages
Open access
Author
Date
2022Type
- Doctoral Thesis
ETH Bibliography
yes
Altmetrics
Abstract
Since software systems increasingly govern both vital infrastructure and people's daily lives, ensuring their safety and security is vital. Where standard measures like testing are insufficient, deductive verification can be used to mathematically prove software properties once and for all. In the past decades, there has been huge progress in the design and automation of verification techniques, to the point where there are multiple automated verification tools able to prove trace properties for statically-typed programming languages like Java or C. However, several challenges remain: Crucial security properties like non-interference are hyperproperties, which are not supported by most standard verification tools. Additionally, new verification techniques have to be developed to enable the verification of programs written in other mainstream programming languages that offer fewer or different static guarantees. In this thesis, we expand the state of the art in these two directions, by enabling the automated verification of hyperproperties in standard verification tools, and making existing verification techniques accessible for the dynamic Python language as well as Ethereum smart contracts.
First, we present a modular verification for Python programs, targeting complex safety and security properties for realistic code. We address the challenges stemming from dynamic typing and the resulting lack of static knowledge about Python programs using a mix of permissive static checks using an unsound type system and additional sound checks in the verifier. The resulting verification technique is able to support typical Python code patterns, and can be integrated with existing specification and verification techniques for safety and security properties. We implement our solution in Nagini, an automated verifier for a substantial subset of Python 3, and demonstrate its ability to verify real-world Python code and prove complex program properties.
Second, we present modular product programs, a program transformation that enables the verification of hyperproperties using standard verification tools. Unlike existing solutions, modular product programs can be constructed automatically, impose no restrictions on program control flow, and, crucially, enable modular proofs of hyperproperties using relational specifications. We apply modular product programs to proving non-interference using special information flow specifications, which can express complex properties like value-dependent sensitivity and termination-sensitive non-interference. We implement the product transformation for the Viper verification infrastructure and show that it can prove both information flow properties and other hyperproperties for challenging examples from the literature.
Third, we show how product constructions like the aforementioned modular product programs, which are usually defined for small, sequential languages, can be applied to more complex languages and integrated with existing verification tools that are based on intermediate verification languages (IVLs). The key idea is to perform the product construction on the level of the (simple) IVL instead of the (complex) source language, thus enabling existing tools to verify hyperproperties with little engineering effort. We show that this approach is not always sound, but provide a simple criterion that guarantees soundness and can be easily checked in practice. Furthermore, we show how one can verify non-interference properties of concurrent source programs using sequential product constructions.
We demonstrate the feasibility of this approach by implementing it for Nagini. Our evaluation shows that this extended Nagini implementation, developed with minimal effort, can compete with existing specialized verification tools for non-interference in terms of its expressiveness, while offering acceptable performance.
Fourth, we present a modular specification and verification technique for Ethereum smart contracts, i.e., small programs that execute in the Ethereum blockchain, which typically implement custom resources and resource transfers. Smart contract verification is challenging because contracts execute in an adversarial environment, interacting with malicious outside contracts that can perform re-entrant calls. We present a specification and verification technique that, unlike existing techniques, is sound and precise in this context and does not assume or impose limits on re-entrancy. Furthermore, we expand this technique to enable the contract-modular verification of sets of collaborating contracts for the first time. Finally, we propose a domain-specific specification language that lets users express properties directly in terms of resources and resource transfers, reducing the likelihood of erroneous specifications. We implement our technique in 2vyper, an automated verification tool for the Vyper language (a smart contract language for Ethereum which is distinct from the aforementioned Viper verification language), and demonstrate its ability to verify complex properties of real smart contracts. Show more
Permanent link
https://doi.org/10.3929/ethz-b-000580641Publication status
publishedExternal links
Search print copy at ETH Library
Contributors
Examiner: Müller, Peter
Examiner: Basin, David
Examiner: Huisman, Marieke
Examiner: Murray, Toby
Publisher
ETH ZurichSubject
VERIFICATION (SOFTWARE ENGINEERING); information flow; Python (programming language); Smart ContractsOrganisational unit
03653 - Müller, Peter / Müller, Peter
More
Show all metadata
ETH Bibliography
yes
Altmetrics