Software Verification

For digital trust to work in practice, the underlying design and implementation need to work even in adversarial scenarios. Formal verification tools systematically analyse all possible scenarios in a formally defined threat model. They can automatically identify previously overlooked lines of attack that require changes to protocols and designs. In the final system, they can mathematically prove that the system continues to deliver the desired functionality in all scenarios. A particular strength of formal verification tools is that they ensure, in combination with compilers and a runtime platform, that the desired functionality is correctly implemented in code running on the deployed system. This approach prevents some of the most widespread cyber-attacks that result from software vulnerabilities such as buffer overflows and ensures that correct high-level protocols cannot be subverted due to implementation bugs.

In this pillar we aim to work on practical formal verification tools applicable to software in general, as well as verified platform that will help industry make a leap towards bullet-proof software implementing digital trust services. Our methodology stems from an observation that the only practical approach to verified software is embedding verification in the software development process itself, by deploying verifiers that work along the compilers and development environments and increasing the automation of verification to make it non-intrusive for developers. We aim to deliver verification tools that can prove safety, security, and privacy properties in an increasingly broad set of scenarios. We also aim to develop techniques to verify specific properties and libraries of interest for the financial industry, for data mining in pharmaceutical industry, and for automated processing of large value chains.

To take one possible example, consider how the emergence of smart contracts (on platforms such as Ethereum) amplifies the need to obtain high confidence in program correctness. When “code is the law”, a mistake in the code can lead to the collapse of an autonomous entity. Indeed, the spectacular logical error in the smart contract program defining the Distributed Autonomous Organization, DAO, has led not only to loss of investment but to forking of the underlying blockchain, shaking the trust in the Ethereum market.

Several prominent players in smart contracts have well recognized the need for verification and validation tools and are engaging with academic collaborators to drive their development. These tools can be used to validate smart contracts, transaction protocols, as well as software implementations of clients performing blockchain computations. Several industrial users have recognized the Scala programming language, developed at EPFL, as a great platform for smart contracts, which makes verification tools such as stainless.epfl.ch of immediate interest for creating trustworthy smart contracts. At the same time, we aim to improve our verification techniques and apply them to a diverse set of software layers and applications, because benefits of verified software are the greatest when applied to the entire software stack.