Rich specifications for Ethereum smart contract verification

Smart contracts are programs that execute in blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that rarely arise in other application domains. Smart contracts frequently interact with unverified, potentially adversarial outside code, which substantially weakens the assumptions that formal analyses can (soundly) make. Moreover, the core functionality of smart contracts is to manipulate and transfer resources; describing this functionality concisely requires dedicated specification support. Current reasoning techniques do not fully address these challenges, being restricted in their scope or expressiveness (in particular, in the presence of re-entrant calls), and offering limited means of expressing the resource transfers a contract performs. In this paper, we present a novel specification methodology tailored to the domain of smart contracts. Our specifications and associated reasoning technique are the first to enable: (1) sound and precise reasoning in the presence of unverified code and arbitrary re-entrancy, (2) modular reasoning about collaborating smart contracts, and (3) domain-specific specifications for resources and resource transfers, expressing a contract's behaviour in intuitive and concise ways and excluding typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in Vyper, and demonstrated its effectiveness for verifying strong correctness guarantees for real-world contracts.

Technical Specification Methodology for an Automotive Proving Ground Dedicated to Connected and Automated Vehicles

Today’s vehicles already have several driver assistant systems and in the near future highly automated vehicles will also appear in road transport. Higher automation levels rely on disruptive technologies that cannot be tested and approved in the former way. To be able to guarantee future road safety also disruptive testing and validation methods are required. The complexity of the systems and the stochasticity of the potential traffic situations demand new approaches with different testing levels and approval layers. Since there are no off-the-self solutions available beyond the research the authors also participate in international activities like the Gear 2030 EU level initiative. This paper will discuss the proposed new approach for connected and automated vehicle testing methodology concluding with the technical specification results for the new Hungarian automotive proving ground.