Cache Side-Channel Attacks (CSCAs) can leak sensitive information by exploiting shared cache resources. Although many secure cache designs like CEASER, ScatterCache, PhantomCache, MIRAGE, and IECache have been proposed, the security evaluation methods being used by these designs remain diverse, often inconsistent, and scattered. This inconsistency makes it challenging to compare the security strengths of the state-of-the-art cache designs for security-critical applications. To address this challenge, we propose a novel consistent security evaluation methodology, called the UniSEC (Unified methodology for Security Evaluation of Caches), which estimates Worst-Case Leakage (WCL) and provides a consistent, comprehensive, and realistic measure of potential information leakage that various cache designs exhibit. UniSEC empirically shows that WCL estimation maximizes the revelation of potential information leakage that Relative Eviction Entropy (REE) based method fails to capture. UniSEC introduces an Effective Security Score (ESS) that takes into account Active Attacker’s Cache Lines (AACLs) within an attacker’s eviction set and the uniformity of the eviction distribution across the AACLs to measure the worst-case leakage. Our results show that well-distributed eviction probabilities across attacker’s eviction set lead to higher ESS and overall entropy. We carry out experiments to measure WCL, REE, and ESS in six state-of-the-art secure cache designs and vary associativity and cache sizes to measure the impact on information leakage. Our experiments reveal that security-critical applications cannot rely on the security guarantees being provided by REE alone. Therefore, WCL is a more realistic metric for measuring the actual amount of information leakage in caches.

We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence “While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career.” We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these. In this paper, we aim to highlight why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the trade-offs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly the supported by Formal Methods.

Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars' worth of transactions. As for every computer program, smart contracts may contain bugs which can be exploited. However, since smart contracts are often used to automate financial transactions, such exploits may result in huge economic losses. In general, it is estimated that since 2019, more than $5B was stolen due to vulnerabilities in smart contracts. This article addresses the issue of smart contract vulnerabilities by introducing an executable denotational semantics for Solidity within the Isabelle/HOL interactive theorem prover. This formal semantics serves as the basis for an interactive program verification environment for Solidity smart contracts. To evaluate our semantics, we integrate grammar-based fuzzing with symbolic execution to automatically test it against the Solidity reference implementation. The article concludes by showcasing the formal verification of Solidity programs, exemplified through the verification of a basic Solidity token.

In protocol verification, we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants such as Isabelle/HOL. The latter provides overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely, and thus the risk of erroneously verifying a flawed protocol is nonnegligible. There are a few works that try to combine the advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step toward achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge, this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results, such as the soundness of a typed model.

Modern supply chains of goods and services rely heavily on close collaborations between the partners within these supply chains. Consequently, there is a demand for IT systems that support collaborations between business partners, for instance, allowing for joint computations for global optimizations (in contrast to local optimizations that each partner can do on their own). Still, businesses are very reluctant to share data or connect their enterprise systems to allow for such joint computation. The topmost factor that businesses name as reason for not collaborating, is their security concern in general and, in particular, the confidentiality of business critical data. While there are techniques (e.g., homomorphic encryption or secure multiparty computation) that allow joint computations and, at the same time, that are protecting the confidentiality of the data that flows into such a joint computation, they are not widely used. One of the main problems that prevent their adoption is their perceived performance overhead. In this paper, we address this problem by an approach that utilized the structure of supply chains by decomposing global computations into local groups, and applying secure multiparty computation within each group. This results in a scalable (resulting in a significant smaller runtime overhead than traditional approaches) and secure (i.e., protecting the confidentiality of data provided by supply chain partners) approach for joint computations within supply chains. We evaluate our approach using life-cycle assessment (LCA) as a case study. Our experiments show that, for instance, secure LCA computations even in supply chains with 15 partners are possible within less than two minutes, while traditional approaches using secure multiparty computation need more than a day.

Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. The framework consists of a novel formalization of the Solidity storage model, a shallow embedding of Solidity expressions and statements, an implementation of Isabelle commands to support a user in specifying Solidity smart contracts, and a verification condition generator to support a user in the verification. Compliance of the semantics is tested by a set of unit tests and the approach is evaluated by means of three case studies. Our results show that the framework can be used to verify even complex contracts with reasonable effort. Moreover, they show that the shallow embedding significantly reduces the verification effort compared to an alternative approach based on a deep embedding.

Isabelle/DOF is an ontology framework on top of Isabelle/HOL. It allows for the formal development of ontologies and continuous conformity-checking of integrated documents, including the tracing of typed meta-data of documents. Isabelle/DOF deeply integrates into the Isabelle/HOL ecosystem, allowing to write documents containing (informal) text, executable code, (formal and semiformal) definitions, and proofs. Users of Isabelle/DOF can either use HOL or one of the many formal methods that have been embedded into Isabelle/HOL to express formal parts of their documents. In this paper, we extend Isabelle/DOF with annotations of lambda-terms, a pervasive data-structure underlying Isabelle to syntactically represent expressions and formulas. We achieve this by using Higher-order Logic (HOL) itself for query-expressions and data-constraints (ontological invariants) executed via code-generation and reflection. Moreover, we add support for parametric ontological classes, thus exploiting HOL's polymorphic type system. The benefits are: First, the HOL representation allows for flexible and efficient run-time checking of abstract properties of formal content under evolution. Second, it is possible to prove properties over generic ontological classes. We demonstrate these new features by a number of smaller ontologies from various domains and a case study using a substantial ontology for formal system development targeting certification according to CENELEC 50128.

In this paper, we report on our experience of teaching formal methods as part of an introductory computer and network security module. This module is part of an applied undergraduate computer science degree. As a consequence, we neither can rely on strong theoretical or mathematical foundations of the students, nor can we focus the whole term on applying formal methods in security. We address these challenges by integrating formal methods into a three-week-long section on security protocols. In these three weeks, we use a holistic approach for teaching the security objectives of security protocols, their analysis of actual implementations using a network sniffer, their formal verification using a model checker (and comparing it to an approach based on interactive theorem proving). Our approach has been proven successful in teaching (both, in-person and remotely) the benefits of formal methods to numerous students. The students do perform well in the corresponding assessments, and each year we are able to attract students for final year projects (i.e., their B.Sc. thesis) in the area of formal methods.

Interval arithmetic is a well known mathematical technique to analyse or mitigate rounding or measurement errors. Thus, it is promising to integrate interval analysis into program verification environments. Such an integration is not only useful for the verification of numerical algorithms: the need to ensure that computations stay within certain bounds is common. For example, to show that arithmetic computations stay within the hardware bounds of a given number representation. We present a formalisation of (extended) interval arithmetic in Isabelle/HOL, including the concept of inclusion isotone (extended) interval analysis. The main result of this part is the formal proof that interval-splitting converges for Lipschitz-continuous interval isotone functions. We also show how interval types can be used for verifying programs in a C-like programming language.

In this paper, we report on our experience of teaching formal methods as part of an introductory computer and network security module. This module is part of an applied undergraduate computer science degree. As a consequence, we neither can rely on strong theoretical or mathematical foundations of the students, nor can we focus the whole term on applying formal methods in security. We address these challenges by integrating formal methods into a three-week-long section on security protocols. In these three weeks, we use a holistic approach for teaching the security objectives of security protocols, their analysis of actual implementations using a network sniffer, their formal verification using a model checker (and comparing it to an approach based on interactive theorem proving). Our approach has been proven successful in teaching (both, in-person and remotely) the benefits of formal methods to numerous students. The students do perform well in the corresponding assessments, and each year we are able to attract students for final year projects (i.e., their B.Sc. thesis) in the area of formal methods.

Isabelle/DOF is an ontology framework on top of Isabelle. It allows for the formal development of ontologies as well as continuous conformity-checking of integrated documents annotated by ontological data. An integrated document may contain text, code, definitions, proofs, and user-programmed constructs supporting a wide range of formal methods Isabelle/DOF is designed to leverage traceability in integrated documents by supporting navigation in Isabelle’s IDE as well as the document generation process. In this paper, we extend Isabelle/DOF with annotations of λ -terms, a pervasive data-structure underlying Isabelle used to syntactically represent expressions and formulas. Rather than introducing an own programming language for meta-data, we use Higher-order Logic (HOL) for expressions, data-constraints, ontological invariants , and queries via code-generation and reflection. This allows both for powerful query languages and logical reasoning over ontologies in, for example, ontological mappings. Our application examples cover documents targeting formal certifications such as CENELEC 50128, or Common Criteria.

Neural networks are being used successfully to solve classification problems, e.g., for detecting objects in images. It is well known that neural networks are susceptible if small changes applied to their input result in misclassification. Situations in which such a slight input change, often hardly noticeable by a human expert, results in a misclassification are called adversarial examples. If such inputs are used for adversarial attacks, they can be life-threatening if, for example, they occur in image classification systems used in autonomous cars or medical diagnosis. Systems employing neural networks, e.g., for safety or security-critical functionality, are a particular challenge for formal verification, which usually expects a formal specification (e.g., given as source code in a programming language for which a formal semantics exists). Such a formal specification does, per se, not exist for neural networks. In this paper, we address this challenge by presenting a formal embedding of feedforward neural networks into Isabelle/HOL and discussing desirable properties for neural networks in critical applications. Our Isabelle-based prototype can import neural networks trained in TensorFlow, and we demonstrate our approach using a neural network trained for the classification of digits on a dot-matrix display.

Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation. While many typical components like TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure. The main goal of compositionality is thus a theorem of the form: given a set of components that are already proved secure in isolation and that satisfy a number of easy-to-check conditions, then also their parallel composition is secure. Said conditions should of course also be realistic in practice, or better yet, already be satisfied for many existing components. Another benefit of compositionality is that when one would like to exchange a component with another one, all that is needed is the proof that the new component is secure in isolation and satisfies the composition conditions—without having to re-prove anything about the other components. This article has three contributions over previous work in parallel compositionality. First, we extend the compositionality paradigm to stateful systems : while previous approaches work only for simple protocols that only have a local session state, our result supports participants who maintain long-term databases that can be shared among several protocols. This includes a paradigm for declassification of shared secrets . This result is in fact so general that it also covers many forms of sequential composition as a special case of stateful parallel composition. Second, our compositionality result is formalized and proved in Isabelle/HOL, providing a strong correctness guarantee of our proofs. This also means that one can prove, without gaps, the security of an entire system in Isabelle/HOL, namely the security of components in isolation and the composition conditions, and thus derive the security of the entire system as an Isabelle theorem. For the components one can also make use of our tool PSPSP that can perform automatic proofs for many stateful protocols. Third, for the compositionality conditions we have also implemented an automated check procedure in Isabelle.

A common problem in verification is to ensure that the formal specification models the real-world system, i.e., the implementation, faithfully. Testing is a technique that can help to bridge the gap between a formal specification and its implementation. Fuzzing in general and grammar-based fuzzing in particular are successfully used for finding bugs in implementations. Traditional fuzzing applications rely on an implicit test specification that informally can be described as “the program under test does not crash”. In this paper, we present an approach using grammar-based fuzzing to ensure the conformance of a formal specification, namely the formal semantics of the Solidity Programming language, to a real-world implementation. For this, we derive an executable test-oracle from the formal semantics of Solidity in Isabelle/HOL. The derived test oracle is used during the fuzzing of the implementation to validate that the formal semantics and the implementation are in conformance.

The environmental impact of products is an important factor in buying decisions of customers and it is also an increasing concern of law makers. Hence, companies are interested in determining the ecological footprint of their products. Life-cycle assessment (LCA) is a standardized method for computing the ecological footprint of a product. Today, LCA is usually not computed in real-time and neither is LCA using actual sensor data: in contrast it is computed “offline” using “historic” values based on exemplary measurements. With the rise of the Internet of Things (IoT), LCA computations can be based on actual production processes. While an LCA based on actual sensor data is desirable from an ecological perspective, it also can reveal trade secrets, e.g., details about production processes or business relationships. In this paper, we present an approach, using secure multi-party computation, to enable the confidential data sharing required for an LCA computation using sensor data.