This report describes an Isabelle/HOL formalization of a STARK-style transparent proof protocol. The development contains an executable model of the prover and verifier, a finite probabilistic state monad with a weakest-precondition calculus, a zero-failure honestcompleteness theorem, and a staged soundness theorem with an explicit probability bound. The report is written for readers with a formal-methods background. It gives enough cryptographic context to explain the protocol, but its main emphasis is the formal model, the decomposition of the proofs, and the Isabelle source locations of the principal definitions and theorems.

Smart contracts are an important innovation in Blockchain which allow to automate financial transactions. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars' worth of transactions. Thus, bugs in smart contracts may lead to high financial losses and it is important to get them right before deploying them to the Blockchain. To address this problem we developed Isabelle/Solidity, a tool for the verification of smart contracts in Isabelle. The tool is implemented as a definitional extension for the Isabelle proof assistant and thus complements existing tools in this area which are mostly based on axiomatic approaches. In this paper we describe Isabelle/Solidity and demonstrate it by verifying a casino contract from the VerifyThis long term verification challenge.

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. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we verify a theorem which guarantees that all instances of an arbitrary contract type satisfy a corresponding invariant. The theorem can be used to verify invariants for Solidity smart contracts. This is demonstrated by a case study in which we use our approach to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.

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.

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.

Smart contracts are programs stored on the blockchain that are often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions; thus, bugs can lead to large financial losses. In previous works, we developed a formalization of Solidity in Isabelle/HOL, which can be used to verify the properties of Solidity smart contracts. This formalization features untyped stores, where the types are inferred using a type environment. It is currently unclear whether our semantics can cause type inconsistencies between stores and their environments. With this work we address this problem by formalizing the notion of type safety for untyped stores and verifying that our semantics preserve this property. The formalization and proofs were verified using Isabelle/HOL. Our results guarantee that our semantics are type safe and the proofs can be used to simplify the verification process for the properties of Solidity smart contracts.

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.

A blockchain acts as a universal ledger for digital transactions between two parties that require no moderation from a third party. Such transactions are cheaper, quicker, and more secure with high traceability and transparency, with the decentralised structure of a blockchain network allowing for greater scalability and availability. For these reasons, blockchain is at the forefront of emerging technologies, with a wide variety of industries investing billions into the technology. A blockchains consensus protocol is what allows a blockchain network to be decentralised but can be subject to malicious behaviour and faults in its design and implementation that can lead to catastrophic effects like the DAO hack that resulted in a loss of $60 million. From this it is clear to see that the verifications of these protocols are paramount to ensure the safe use of blockchain. In this research, we formally verify the Proof-of-Work consensus protocol, used by Bitcoin, in Isabelle/HOL by modelling the blockchain as the longest branch in a binary tree and proving that the common prefix property holds with the assumption that the network is in majority honest. In this paper, we discuss the validity of our approach, key functions and lemmas we used to complete the proof, advantages and drawbacks of the model, related work and how this research can be taken further.

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.

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. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we describe a Verification Condition Generator to automate the use of the calculus. Our approach can be used to verify the functional correctness of Solidity smart contracts. To demonstrate this, we use it to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.

Motivation: Smart grids design requires energy distribution operations to be adaptable to abnormality. This requirement entails distribution system operators (DSOs) to optimize restoration to normal operational states dynamically. However, these design challenges demand collaborative research efforts on sophisticated modeling and simulation approaches. Approach: In the ESOSEG research project, analyzing the smart grid domain as a software-intensive system, we employed a dynamic architecture approach, particularly the FOCUS theory, to model and assure the domains' self-healing requirements. Although some works specify various self-healing systems, to the best of our knowledge, the use of the approach in smart grids is the first work to enable a formal specification and verification of self-healing properties in smart grids. Results: As a result, to support the modeling and verification process, we developed tool support with Eclipse Modeling Framework (EMF), Xtext, and other languages in the EMF ecosystem. The tool includes a grammar or a meta-model of the DSL, an interface to enable textual and graphical modeling of architectural patterns and code transformer engine for verification. Furthermore, we evaluated the modeling and verification features of the tool support with an e-Car charging scenario for modeling adaptive self-healing properties. Futureworks: As an outlook, future works could include investigation of comprehensive case studies. These, for instance, could be further particular adaptability scenarios addressing challenges in DSOs. Another interesting aspect could be the evaluation of the modeling approach by investigating its use with engineers involved in a smart grid design. Next, the evaluation could be followed with abstractions of the verification process to make it useable by system architects with no knowledge of the proof language, Isabelle/HOL.

The Model Curricula Subcommittee of the IEEE Computer Society Education Committee was formed some 16 months ago to develop an IEEE Computer Society-sanctioned four-year curriculum in computer science and engineering to be used by colleges and ...

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.

Smart contracts are programs, usually automating legal agreements such as financial transactions. Thus, bugs in smart contracts can lead to large financial losses. For example, an incorrectly initialized contract was the root cause of the Parity Wallet bug that made USD 280mil worth of Ether inaccessible. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts. In this paper, we address this problem by presenting an executable denotational semantics for Solidity in the interactive theorem prover Isabelle/HOL. This formal semantics builds the foundation of an interactive program verification environment for Solidity programs and allows for inspecting Solidity programs by (symbolic) execution. We combine the latter with grammar-based fuzzing to ensure that our formal semantics complies to the Solidity implementation on the Ethereum Blockchain. Finally, we demonstrate the formal verification of Solidity programs by two examples: constant folding and memory optimization.

The architecture of a system captures important design decisions for the system. Over time, changes in a system's implementation may lead to violations of specific design decisions. This problem is common in industry and known as architectural erosion. Since it may have severe consequences on the quality of a system, research has focused on the development of tools and techniques to address the presented problem. As of today, most of the approaches to detect architectural erosion employ static analysis techniques. While these techniques are well-suited for the analysis of static architectures, they reach their limit when it comes to dynamic architectures. Thus, in this paper, we propose an alternative approach based on runtime verification: We describe techniques to formally specify constraints for dynamic architectures and algorithms to translate such specifications to instrumentation code and corresponding monitors. The approach is implemented in Eclipse/EMF, demonstrated through a running example, and evaluated using two case studies.