EPICURE

The frequent announcements of yet another cybersecurity breach show that the security of the software that surrounds us is, more than ever, a scientific challenge of utmost societal importance. More and more software is produced to operate on an increasingly varied number of devices and to provide increasingly complex functionality. 

The goal of the EPICURE project is to contribute with semantics-based methods for producing safe and secure software by defining new semantic frameworks that will provide more accurate models of modern execution platforms. This will
serve to model safety and security properties related to information flow control and side channels, and to design formally verified analysis and compilation schemes.

The specific aim is to analyse and verify properties of programs written in high-level languages, and to compile both program and the verified properties down to low-level executable representations. We will demonstrate the impact of
language-based tools on software security by showing how they can improve the correctness, safety and security of critical software found in modern execution environments, such as the Java virtual machine, the Tezos blockchain written in OCaml, and small operating systems for the IoT such as RIOT.