Leveraging Applications of Formal Methods, Verification and Validation: Applications

The rise of smart contracts executed on blockchain and other distributed ledger technologies enabled trustless yet decentralised computation. Various applications take advantage of this computational model, including enforced financial contracts, self-sovereign identity and voting. But smart contracts are nothing but software running on a blockchain, with risks of malfunction due to bugs in the code. Compared to traditional systems, there is an additional risk in that erroneous computation or transactions triggered by a smart contract cannot be easily rolled back due to the immutability of the underlying execution model. This ISoLA track brings together a number of experts in the field of smart contract reliability and verification to discuss the state-of-the-art in smart contract dependability and discuss research challenges and future directions.

We present an invariant-based specification and verification methodology that allows us to conveniently specify and verify strong data integrity properties for Solidity smart contracts. Our approach is able to reason precisely about arbitrary usage of the contracts, which may include re-entrance, a common security pitfall in smart contracts. We implemented the approach in a prototype verification tool, called SolidiKeY, and applied it successfully to a number of smart contracts.

Covenants are linguistic primitives that extend the Bitcoin script language, allowing transactions to constrain the scripts of the redeeming ones. Advocated as a way of improving the expressiveness of Bitcoin contracts while preserving the simplicity of the UTXO design, various forms of covenants have been proposed over the years. A common drawback of the existing descriptions is the lack of formalization, making it difficult to reason about properties and supported use cases. In this paper we propose a formal model of covenants, which can be implemented with minor modifications to Bitcoin. We use our model to specify some complex Bitcoin contracts, and we discuss how to exploit covenants to design high-level language primitives for Bitcoin contracts.

Smart contracts are programs which run in conjunction with distributed ledgers. They often manage valuable assets, but, like all programs, they contain errors which can be exploited by an attacker. This makes them are a prime target for formal methods. Many formal analysis methods require the contracts’ program code to be annotated with formal specifications. In this paper, we propose an approach and a formalism to enrich specifications with frame conditions, i.e., a specification of what a smart contract function cannot resp. will not do. We discuss the storage models of two smart contract platforms, Ethereum and Hyperledger Fabric, and propose languages for specifying frame conditions for both of them, based on the theory of dynamic frames.

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Coq proof assistant to have stronger guarantees on Michelson smart contracts: the Mi-Cho-Coq framework, a Coq library defining formal semantics of Michelson, as well as an interpreter, a simple optimiser and a weakest-precondition calculus to reason about Michelson smart contracts; Albert, an intermediate language that abstracts Michelson stacks with a compiler written in Coq that targets Mi-Cho-Coq.

We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.

User-defined tokens—both fungible ERC-20 and non-fungible ERC-721 tokens—are central to the majority of contracts deployed on Ethereum. User-defined tokens are non-native on Ethereum; i.e., they are not directly supported by the ledger, but require custom code. This makes them unnecessarily inefficient, expensive, and complex.

The Extended UTXO Model (EUTXO)  [5] has been introduced as a generalisation of Bitcoin-style UTXO ledgers, allowing support of more expressive smart contracts, approaching the functionality available to contracts on Ethereum. Specifically, a bisimulation argument established a formal relationship between the EUTXO ledger and a general form of state machines. Nevertheless, transaction outputs in the EUTXO model lock integral quantities of a single native cryptocurrency only, just like Bitcoin.

In this paper, we study a generalisation of the EUTXO ledger model with native user-defined tokens. Following the approach proposed in a companion paper  [4] for the simpler case of plain Bitcoin-style UTXO ledgers, we generalise transaction outputs to lock not merely coins of a single cryptocurrency, but entire token bundles, including custom tokens whose forging is controlled by forging policy scripts. We show that this leads to a rich ledger model that supports a broad range of interesting use cases.

Our main technical contribution is a formalisation of the multi-asset EUTXO ledger in Agda, which we use to establish that the ledger with custom tokens is strictly more expressive than the original EUTXO ledger. In particular, we state and prove a transfer result for inductive and temporal properties from state machines to the multi-asset EUTXO ledger, which was out of scope for the single-currency EUTXO ledger. In practical terms, the resulting system is the basis for the smart contract system of the Cardano blockchain.

A prominent use case of Ethereum smart contracts is the creation of a wide range of user-defined tokens or assets by way of smart contracts. User-defined assets are non-native on Ethereum; i.e., they are not directly supported by the ledger, but require repetitive custom code. This makes them unnecessarily inefficient, expensive, and complex. It also makes them insecure as numerous incidents on Ethereum have demonstrated. Even without stateful smart contracts, the lack of perfect fungibility of Bitcoin assets allows for implementing user-defined tokens as layer-two solutions, which also adds an additional layer of complexity.

In this paper, we explore an alternative design based on Bitcoin-style UTXO ledgers. Instead of introducing general scripting capabilities together with the associated security risks, we propose an extension of the UTXO model, where we replace the accounting structure of a single cryptocurrency with a new structure that manages an unbounded number of user-defined, native tokens, which we call token bundles. Token creation is controlled by forging policy scripts that, just like Bitcoin validator scripts, use a small domain-specific language with bounded computational expressiveness, thus favouring Bitcoin’s security and computational austerity. The resulting approach is lightweight, i.e., custom asset creation and transfer is cheap, and it avoids use of any global state in the form of an asset registry or similar.

The proposed UTXO\(_{\textsf {ma}}\) model and the semantics of the scripting language have been formalised in the Agda proof assistant.

Runtime Verification in both traditional systems and smart contracts has typically been implemented at the application level. Such systems very often run on Virtual Machines which execute their application logic. Conditional monitoring is often implemented to enable for certain monitors to be switched off in aim of reducing execution overheads once certain levels of assurance have been provided. Even when turned off such application level conditional monitoring still incurs added overheads to execute the conditional statement related operations. In this paper, we propose methods to support conditional runtime verification of applications at the virtual machine level. We demonstrate that such an approach can provide lower overheads in terms of both execution and gas.

Michelson, the stack-based virtual machine of the Tezos blockchain, integrates type-checking for program execution completion but not program correctness. Manual stack tracking is efficient but less ergonomic to write in than a higher-level lambda calculus with variables. Compiling McBride’s Quantitative Type Theory to Michelson allows for compile-time verification of semantic predicates and automatic stack optimisation by virtue of the type-theoretic usage accounting system.

SMT solvers can verify properties automatically and efficiently, and they offer increasing flexibility on the ways those properties can be described. But it is hard to predict how those ways of describing the properties affect the computational cost of verifying them.

In this paper, we discuss what we learned while implementing and optimising the static analysis for Marlowe, a domain specific language for self-enforcing financial smart-contracts that can be deployed on a blockchain.

Smart contracts challenge the existing, highly efficient techniques applied in symbolic model checking of software by their unique traits not present in standard programming models. Still, the majority of reported smart contract verification projects either reuse off-the-shelf model checking tools resulting in inefficient and even unsound models, or apply generic solutions that typically require highly-trained human intervention. In this paper, we present the solution adopted in the formal analysis engine of the official Solidity compiler. We focus on the accurate modeling of the central aspects of smart contracts. For that, we specify purpose-built rules defined in the expressive and highly automatable logic of constrained Horn clauses, which are readily supported by an effective solving infrastructure for establishing sound safety proofs or finite-length counterexamples. We evaluated our approach on an extensive set of smart contracts recently deployed in the Ethereum platform. The reported results show that the approach is able to prove correctness and discover bugs in significantly more contracts than comparable publicly available systems.

In this paper, we present a framework for the development of on-chain forwards (and futures). This utilises smart contracts to automate the custody of collateral and settlement of payouts on expiry. Importantly, our framework also enables forwards to be traded without counterparty risk or reliance on off-chain assets (such as fiat currencies). To achieve this, we build on our previous work on on-chain options and demonstrate how the relevant mathematical guarantees can be extended to forwards. In addition, we discuss recent trends in cryptoasset derivatives, capital requirements, and other design considerations (such as the use of split contracts). This paper will be of interest to academics and practitioners interested in financial smart contracts.

Embedded control software is used in a variety of industries, such as in the automotive and railway domains, or in industrial automation and robotization. The development of such software is subject to tight time-to-market requirements, but at the same time also to very high safety requirements posed by various safety standards. To assure the latter, formal methods such as model-based testing and formal verification are increasingly used. However, the main obstacle to a more wide-scale adoption of these methods, and especially of formal verification, is the currently relative low level of automation of the verification process and integration in the general software development cycle. At present, writing formal specifications and annotating the embedded code is still a highly labour intensive activity requiring special competence and skills. In this track we address this challenge from various angles. We start by introducing the topic and then give a summary of the contributions.

This paper describes a model-based flow for the development of Interlocking Systems. The flow starts from a set of specifications in Controlled Natural Language (CNL), that are close to the jargon adopted in by domain experts, but fully formal. From the CNL, a complete SysML specification is extracted, leveraging various forms of diagrams, and enabling automated code generation. Several formal verification methods are supported. A complementary part of the flow supports the extraction of formal properties from legacy Interlocking Systems designed as Relay circuits. The flow is implemented in a comprehensive toolset, and is currently used by railway experts.

Emerging smart technologies add elements of intelligence, cooperation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes. Hybrid automata, in their various flavours, have been suggested as a formal model accurately capturing CPS dynamics and thus facilitating exhaustive behavioural analysis of interacting CPSes with mathematical rigour.

In this article, we demonstrate that despite their expressiveness, all flavours of hybrid automata fall short of being able to accurately capture the interaction dynamics of systems of well-engineered, rationally acting CPS designs. The corresponding verification verdicts obtained on the best possible approximations of the actual CPS dynamics are across the range of hybrid-automata models bound to be either overly optimistic or overly pessimistic, i.e., imprecise.

We identify inaptness to accurately represent rational decision-making under uncertain information as the cause of this deficiency. Such rational decision-making requires manipulation of state distributions representing environmental state estimates within the system state itself. We suggest a corresponding extension of hybrid automata and discuss the problem of providing automatic verification support.

Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team’s learning curve for this experiment and present the preliminary conclusions on the case study.

Assuring the safety of an automated driving system is difficult, because a large, heterogeneous set of traffic situations has to be handled by the system. Systematic testing of the full system at the end of the development seems necessary to be able to reach the required level of assurance. In our approach, the set of potentially relevant, concrete test cases result by parameter instantiation from finitely many more abstract, so called logical scenarios. For nearly all interesting automation systems, even virtual testing via simulation can cover only a tiny fraction of this set of concrete test cases.

Here we present an approach by which a selection of test cases can be shown to be sufficient to assert the system’s safety. For that, we make reasonable assumptions about the system’s inner workings, and about the way safety of a traffic situation can be captured mathematically. Based on these assumptions a criterion for test coverage is derived. This criterion can be used in a simulation procedure exploring the scenario space as a stop condition. If some additional conditions are met, the criterion is shown to imply sufficient coverage to assert safety of the system under test. We discuss the extent and limitation of the resulting guarantee.

We plan to elaborate, implement, and demonstrate this procedure in the context of research projects which develop and apply simulation tools for the verification and validation of automated driving systems.

The verification of hybrid embedded control systems is a difficult and time intensive task. In previous work, we have presented a compositional, service-oriented verification approach for hybrid systems that are modeled in Simulink using differential dynamic logic and the interactive theorem prover KeYmaera X. In this paper, we discuss the challenges that arise during this verification process with a hybrid system from the medical domain, namely a generic infusion pump (GIP). We discuss the manual effort necessary to verify this (comparatively large) system and propose partial automations that reduce the effort and increase the practical applicability of the verification process.

In this paper, we present a methodology for the verification of safety properties of robotic plans in household environments by a combination of environment reasoning using Discrete Event Calculus (DEC) and Symbolic Execution for effectively handling symbolic input variables (e. g. object positions). We demonstrate the applicability of our approach in an experimental evaluation by verifying safety properties of robotic plans controlling a two-armed, human-sized household robot packing and unpacking a shelf. Our experiments demonstrate our approach’s capability to verify several robotic plans in a realistic, logically formalized environment.

Based upon first-order logic, the paper presents a methodology and a deductive system for proving compositionality. Typical specifications found in industry are not expressed in any formal notation; rather most often in natural language. Therefore, the methodology does not assume specifications to be formal logical sentences. Instead, the methodology takes as input, properties of specifications and in particular, refinement relations. To cover general industrial heterogeneous systems, the semantics chosen is behavior based, originating in previous work on contract-based design for cyber-physical systems. In contrast to the previous work, implementation of specifications is non-monotonic with respect to composition. That is, even though a specification is implemented by one component, a composition with a second component may not implement the same specification. This kind of non-monotonicity is fundamentally important to support architectural specifications and so-called freedom-of-interference used in design of safety critical systems.

A collaborative embedded system is an autonomous component of a cyber-physical system which cooperates with other such systems in order to accomplish a common goal. In this paper, we report on approaches for the validation of such collaborative embedded systems. We describe specification methods for hierarchies of goals and targets. Using model checking of alternating signal temporal logic, we show how to construct strategies for the satisfaction of goals and targets. For runtime validation of safety properties, we give a robust monitoring procedure which can flag potential problems in advance. Our two examples are car platooning and automated guided vehicles in industrial production. In the car platooning example, autonomous vehicles collaborate to enable high-speed driving at short distances. The fleet of transport robots collaborates in loading and unloading of production machines.

The growingly wide deployment of ERTMS-ETCS systems on high speed lines as well as on freight corridors is already a witness to the possible achievement of high safety standards by means of distributed control algorithms, that span over geographical areas and are able to safely control large physical systems.

During the last five years, Event-B formal modelling has been successfully applied to various railway systems to demonstrate safety early in the design process or once systems are in operation. This approach is aimed at formalising a safety reasoning instead of modelling every bit of the system. This approach is intrinsically fit to scale up to large systems (or system of systems), hence able to handle centralised or distributed systems.

The paper studies the use of formal methods in system design engineering in railways. Starting from the use of formal methods in French metro lines, the paper analyses various steps of dissemination of this know-how for main traffic lines. The case study of the ERTMS developments in France is presented for high speed lines and ETCS level 2. A study for an implementation in French regions is also considered. The last project to be analysed is the autonomous train of the IRT Railenium for the SNCF (the French railway national company). The system analysis shows that the old design assumptions are not valid anymore, as the system requires the autonomous trains to process a lot of data. All these industrial needs lead to specify a new approach based on a new semantic link between sub-systems: REFSEES. The main target is to make it possible to focus on a given sub-system refinement while preserving global invariants.

This paper investigates the modelling and model checking of a real-world distributed railway interlocking system algorithm using UPPAAL. Interlocking systems for specific railway networks are verified by instantiating a generic (re-configurable) model with configuration data that describes the network and involved trains. There are three variants of the generic model: (1) The first variant includes the minimum required operations such as reserving a segment for a train, locking a point in a fixed position, and moving a train. (2) A restricted variant that uses a more strict operational order. (3) A variant that extends the first variant with a cancel operation that removes reservations and locks. Verification experiments are carried out on instances of all variants in order to check their correctness and compare their performance. The scalability of the three variants has been investigated with networks of varying sizes. Finally, for a real-world railway network, instances of the three model variants have been successfully verified.

We discuss a new “flavour” of distributed interlocking systems, where the proper interlocking logic is allocated on cloud computers using conventional (i.e. commercial-off-the-shelf) multi-core hardware and operating systems. The servers in the cloud communicate with intelligent track elements over internet connections. Interlocking logic may even be geographically distributed on more than one server farm, introducing a new dimension of fault tolerance. This technology has been announced 2018 by Siemens Mobility, and the certification is currently underway. In this paper, it is analysed how the new distribution concept affects verification, validation, and certification. In particular, the complexity of the cloud system suggests to create a collection of scenario models instead of a single comprehensive model specifying the expected behaviour of the system. The use of scenario models is well known from the autonomous vehicle domain, but, to our best knowledge, it is the first time that this approach is also applied in the railway domain. We discuss verification-related and test-related implications of the scenario approach. In particular, solutions are proposed for determining whether a collection of scenario models is complete, and for deciding whether sufficient test coverage has been achieved for a given scenario. The material presented here is based on a collaboration between Siemens and Verified Systems International, a company specialised on verification and validation of safety-critical systems.

This paper investigates the use of k-induction with RT-Tester for tackling the challenge of verifying the safety of a distributed railway interlocking system. For a real-world case study, it is described how a generic and reconfigurable model of the system is modelled in a new extension of the RAISE Specification Language (RSL). The generic model is instantiated with concrete data sets and subsequently model checked with respect to safety properties using the k-induction facilities in RT-Tester. The performance metrics of the verification with k-induction are additionally compared with the metrics of verifying the same system model with the SAL model checker.

The Shift2Rail Innovation Programme (IP) is focussing on innovative technologies to enhance the overall railway market segments. Formal methods and standard interfaces have been identified as two key concepts to reduce time-to-market and costs, while ensuring safety, interoperability and standardisation. However, the decision to start using formal methods is still deemed too risky. Demonstrating technical and commercial benefits of both formal methods and standard interfaces is necessary to address the obstacles of learning curve and lack of clear cost/benefit analysis that are hindering their adoption, and this is the goal of the 4SECURail project, recently funded by the Shift2Rail IP. In this paper, we provide the reasoning and the rationale for designing the formal methods demonstrator for the 4SECURail project. The design concerns two important issues that have been analysed: (i) the usefulness of formal methods from the point of view of the infrastructure managers, (ii) the adoption of a semi-formal SysML notation within our formal methods demonstrator process.