Formal methods

A software implementation shows side-channel leakage when the physical effects of its implementation have a dependency to secret data such as cryptographic keys. Relevant physical effects include instruction execution time, memory access time, power consumption and electromagnetic radiation. Fifteen years after differential power analysis was first demonstrated, side-channel attacks are affecting software implementations in a broad variety of processors. Yet, without the support of automatic tools, programmers still have to resort to manual and error-prone insertion of countermeasures.

To reduce production cost while meeting time-to-market constraints, semiconductor companies usually design hardware systems with reusable hardware modules, popularly known as Intellectual Property (IP) blocks. Growing reliance on these hardware IPs, often gathered from untrusted third-party vendors, severely affects the security and trustworthiness of the final system. The hardware IPs acquired from external sources may come with deliberate malicious implants, undocumented interfaces working as hidden backdoor, or other integrity issues.

Security protocols enable useful tasks over untrusted networks. For example, confidential communication over the Internet between users and Web services like Google, Facebook, Amazon and Bank of America rely on protocols like SSL/TLS and the supporting Public Key Infrastructure (PKI). These protocols are designed to provide global security properties like authentication and confidentiality when various parties (e.g., the user, the Web service, and participants in the PKI such as certificate authorities) execute their prescribed programs.

Computerized systems are present in various aspects of modern society. These systems are used to access and share confidential information. Such sharing is achieved through cryptographic protocols which often employ randomization to introduce unpredictability in their behavior to achieve critical security objectives and make it difficult for the malicious adversaries to infer the underlying execution of the participants.

Cyberattacks are enabled by software vulnerabilities that allow attackers to plant software exploits. As old vulnerabilities are found and fixed, attackers continue to find new ones. As a result, software vendors, system administrators and security professionals have come to rely increasingly on techniques that insert additional code into software for detecting and/or blocking cyber attacks in progress.