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.

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 ...

Abstract Context Formal methods (FMs) have been around for a while, still being unclear how to leverage their benefits, overcome their challenges, and set new directions for their improvement towards a more successful transfer into practice. Objective We study the use of formal methods in mission-critical software domains, examining industrial and academic views. Method We perform a cross-sectional on-line survey. Results Our results indicate an increased intent to apply FMs in industry, suggesting a positively perceived usefulness. But the results also indicate a negatively perceived ease of use. Scalability, skills, and education seem to be among the key challenges to support this intent. Conclusions We present the largest study of this kind so far ( N = 216), and our observations provide valuable insights, highlighting directions for future theoretical and empirical research of formal methods. Our findings are strongly coherent with earlier observations by Austin and Graeme (1993).

With the emergence of mobile and adaptive computing, dynamic architectures have become increasingly important. In such architectures, components can appear and disappear, and connections between them can change over time. Verification of such architectures is performed over the composition of its components, which is usually defined in an operational style. Sometimes however, a denotational style might be more convenient for verification. Thus, in the following paper, we propose a denotational semantics for composition in dynamic architectures based on fixed points in lattices. We show that it is well-defined by proving that fixed points are guaranteed to exist. Finally, we use our definition to derive a logical characterization of composition, which forms the basis of a framework for the interactive verification of dynamic architectures.

Abstract Architectural design patterns (ADPs) are architectural solutions to common architectural design problems. They are an important concept in software architectures used for the design and analysis of architectures. An ADP usually constrains the design of an architecture and, in turn, guarantees some desired properties for architectures implementing it. Sometimes, however, the constraints imposed by an ADP do not lead to the claimed guarantee. Thus, applying such patterns for the design of architectures might result in architectures which do not fulfill their intended requirements. To address this problem, we propose an approach for the verification of ADPs, based on interactive theorem proving. To this end, we introduce a model for dynamic architectures and a language for the specification of ADPs over this model. Moreover, we propose a framework for the interactive verification of such specifications based on Isabelle/HOL. In addition we describe an algorithm to map a specifi cation to a corresponding Isabelle/HOL theory over our framework. To evaluate the approach, we implement it in Eclipse/EMF and use it for the verification of four ADPs: variants of the Singleton, the Publisher-Subscriber, the Blackboard pattern, and a pattern for Blockchain architectures. With our approach we complement traditional approaches for the verification of architectures, which are usually based on automatic verification techniques such as model checking.

Architectural design patterns capture architectural design experience and provide abstract solutions to recurring architectural design problems. Their description is usually expressed informally and it is not verified whether the proposed specification indeed solves the original design problem. As a consequence, an architect cannot fully rely on the specification when implementing a pattern to solve a certain problem. To address this issue, we propose an approach for the specification and verification of architectural design patterns. Our approach is based on interactive theorem proving and leverages the hierarchical nature of patterns to foster reuse of verification results. The following paper presents FACTum, a methodology and corresponding specification techniques to support the formal specification of patterns. Moreover, it describes an algorithm to map a given FACTum specification to a corresponding Isabelle/HOL theory and shows its soundness. Finally, the paper demonstrates the approach by verifying versions of three widely used patterns: the singleton, the publisher-subscriber, and the blackboard pattern.

In service oriented architectures, components provide services on their output ports and consume services from other components on their input ports. Thereby, a component is said to depend on another component if the former consumes a service provided by the latter. This notion of dependency (which we call syntactic dependency) is used by many architecture analysis tools as a measure for system maintainability. With this paper, we introduce a weaker notion of dependency, still sufficient, however, to guarantee semantic independence between components. Thereby, we discover the concepts of weak and strong semantic dependency and prove that strong semantic dependency indeed implies syntactic dependency. Our alternative notion of dependency paves the way to more precise dependency analysis tools. Moreover, our results about the different types of dependencies can be used for the verification of semantic independence.

In component-based design, temporal logic is a means to specify the temporal behavior of components. If these components are deployed to a dynamic architecture, they can be activated and deactivated over time. Thus, the traditional semantics of temporal specifications of component-behavior does no longer reflect the actual behavior of the components within such dynamic architectures. To address this problem, we provide an alternative semantics of temporal specifications of component-behavior for dynamic architectures, taking into account component activation and deactivation. We show soundness and relative completeness of our semantics w.r.t. the traditional one. The new semantics can then be used to support in the formal specification of dynamic architectures by separating the specification of component-behavior from other aspects such as component activation and architecture reconfiguration.

We consider the problem of achieving a required level of confidence about safety-critical systems consisting of interacting components. Especially, we address restrictions in traditional A/G reasoning techniques which may cause false positives in contract compatibility analyses. Therefore, we introduce interface assertions, i. e., predicate logical formulae over the components' interfaces. We show how to compute interface assertions for architecture configurations based on the interface assertions of the corresponding components and show soundness and relative completeness of the method. Moreover, we introduce mode-based contracts, which - as a special kind of interface assertions - consist of dedicated assume and guarantee pairs. They provide a methodological guidance for developers and facilitate contract specification in contrast to e. g. traditional A/G reasoning. For this concept, we provide algorithms to check under-specification, over-specification, and the fulfillment of specifications. We also sketch how the checks can be operationalized using SMT solvers. Finally, an example demonstrates the approach.

Architectural styles and patterns play an important role in software architectures. However, they are usually only stated informally, which may cause problems such as ambiguity and wrong conclusions. A rigorous theory of architectural styles --- consisting of (i) mathematical models for each style; (ii) axioms to identify different variants of a style; and (iii) rigorous analyses by means of mathematical proofs --- would address these problems. With this work we report on our progress towards such a rigorous theory of architectural styles.