| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
A Unified Approach for Static and Runtime Verification: Framework and Applications
- 2012
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642340253 ; :PART 1, s. 312-326
-
Conference paper (peer-reviewed)abstract
- Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper, we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
|
|
| 2. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Smart Contracts: A Killer Application for Deductive Source Code Verification
- 2018
-
In: Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday. - Cham : Springer International Publishing. - 9783319980478 ; , s. 1-18
-
Book chapter (other academic/artistic)abstract
- Smart contracts are agreements between parties which, not only describe the ideal behaviour expected from those parties, but also automates such ideal performance. Blockchain, and similar distributed ledger technologies have enabled the realisation of smart contracts without the need of trusted parties—typically using computer programs which have access to digital assets to describe smart contracts, storing and executing them in a transparent and immutable manner on a blockchain. Many approaches have adopted fully fledged programming languages to describe smart contract, thus inheriting from software the challenge of correctness and verification—just as in software systems, in smart contracts mistakes happen easily, leading to unintended and undesirable behaviour. Such wrong behaviour may show accidentally, but as the contract code is public, malicious users can seek for vulnerabilities to exploit, causing severe damage. This is witnessed by the increasing number of real world incidents, many leading to huge financial losses. As in critical software, the formal verification of smart contracts is thus paramount. In this paper we argue for the use of deductive software verification as a way to increase confidence in the correctness of smart contracts. We describe challenges and opportunities, and a concrete research program, for deductive source code level verification, focussing on the most widely used smart contract platform and language, Ethereum and Solidity.
|
|
| 3. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Specification language for static and runtime verification of data and control properties
- 2015
-
In: Lecture Notes in Computer Science. FM 2015: FORMAL METHODS. 20th International Symposium on Formal Methods (FM), Oslo, Norway, June 24-26, 2015. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319192482 ; 9109, s. 108-125
-
Conference paper (peer-reviewed)abstract
- Static verification techniques can verify properties across all executions of a program, but powerful judgements are hard to achieve automatically. In contrast, runtime verification enjoys full automation, but cannot judge future and alternative runs. In this paper we present a novel approach in which data-centric and control-oriented properties may be stated in a single formalism, amenable to both static and dynamic verification techniques. We develop and formalise a specification notation, ppDATE, extending the control-flow property language used in the runtime verification tool Larva with pre/post-conditions and show how specifications written in this notation can be analysed both using the deductive theorem prover KeY and the runtime verification tool Larva. Verification is performed in two steps: KeY first partially proves the dataoriented part of the specification, simplifying the specification which is then passed on to Larva to check at runtime for the remaining parts of the specification including the control-centric aspects. We apply the approach to Mondex, an electronic purse application.
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
StaRVOOrS - Episode II: Strengthen and distribute the force
- 2016
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319471655 ; 9952, s. 402-415
-
Conference paper (peer-reviewed)abstract
- Static and runtime techniques for the verification of programs are complementary. They both have their advantages and disadvantages, and a natural question is whether they may be combined in such a way as to get the advantages of both without inheriting too much from their disadvantages. In a previous contribution to ISoLA’12, we have proposed StaRVOOrS (‘Static and Runtime Verification of Object- Oriented Software’), a unified framework for combining static and runtime verification in order to check data- and control-oriented properties. Returning to ISoLA here, we briefly report on advances since then: a unified specification language for data- and control-oriented properties, a tool for combined static and runtime verification, and experiments. On that basis, we discuss two future research directions to strengthen the power, and broaden the scope, of combined static and runtime verification: (i) to use static analysis techniques to further optimise the runtime monitor, and (ii) to extend the framework to the distributed case.
|
|
| 5. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Verification of Smart Contract Business Logic: Exploiting a Java Source Code Verifier
- 2019
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11761 LNCS, s. 228-243
-
Conference paper (peer-reviewed)abstract
- Smart contracts have been argued to be a means of building trust between parties by providing a self-executing equivalent of legal contracts. And yet, code does not always perform what it was originally intended to do, which resulted in losses of millions of dollars. Static verification of smart contracts is thus a pressing need. This paper presents an approach to verifying smart contracts written in Solidity by automatically translating Solidity into Java and using KeY, a deductive Java verification tool. In particular, we solve the problem of rolling back the effects of aborted transactions by exploiting KeY’s native support of JavaCard transactions. We apply our approach to a smart contract which automates a casino system, and discuss how the approach addresses a number of known shortcomings of smart contract development in Solidity.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- 2017
-
In: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 51:1, s. 200-265
-
Journal article (peer-reviewed)abstract
- Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.
|
|
| 7. |
- Chimento, Mauricio, 1985, et al.
(author)
-
STARVOORS: A Tool for Combined Static and Runtime Verification of Java
- 2015
-
In: Lecture Notes in Computer Science - 6th International Conference on Runtime Verification (RV). - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319238203 ; 9333, s. 297-305
-
Conference paper (peer-reviewed)abstract
- We present the tool StaRVOOrS (Static and Runtime Verification of Object-Oriented Software), which combines static and runtime verification (RV) of Java programs. The tool automates a framework which uses partial results extracted from static verification to optimise the runtime monitoring process. StaRVOOrs combines the deductive theorem prover KeY and the RV tool LARVA, and uses properties written using the ppDATE specification language which combines the control-flow property language DATE used in LARVA with Hoare triples assigned to states. We demonstrate the effectiveness of the tool by applying it to the electronic purse application Mondex.
|
|
| 8. |
- Chimento, Mauricio, 1985, et al.
(author)
-
Testing Meets Static and Runtime Verification
- 2018
-
In: Proceedings - 2018 ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018. - New York, NY, USA : ACM. ; , s. 30-39
-
Conference paper (peer-reviewed)abstract
- Test driven development (TDD) is a technique where test cases are used to guide the development of a system. This technique introduces several advantages at the time of developing a system, e.g. writing clean code, good coverage for the features of the system, and evolutionary development. In this paper we show how the capabilities of a testing focused development methodology based on TDD and model-based testing, can be enhanced by integrating static and runtime verification into its workflow. Considering that the desired system properties capture data- As well as control-oriented aspects, we integrate TDD with (static) deductive verification as an aid in the development of the data-oriented aspects, and we integrate model-based testing with runtime verification as an aid in the development of the control-oriented aspects. As a result of this integration, the proposed development methodology features the benefits of TDD and model-based testing, enhanced with, for instance, early detection of bugs which may be missed by TDD, regarding data aspects, and the validation of the overall system with respect to the model, regarding the control aspects.
|
|
| 9. |
- Eshghie, Mojtaba, et al.
(author)
-
Capturing Smart Contract Design with DCR Graphs
- 2023
-
In: Software Engineering and Formal Methods. - : Springer Science and Business Media Deutschland GmbH. ; 14323 LNCS, s. 106-125
-
Conference paper (peer-reviewed)abstract
- Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture the mentioned features. We utilize this expressiveness to show that many common high-level design patterns representing the underlying business processes in smart-contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.
|
|
| 10. |
- Sanchez Perez, Cesar, 1981, et al.
(author)
-
A survey of challenges for runtime verification from advanced application domains (beyond software)
- 2019
-
In: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 1572-8102 .- 0925-9856. ; 54:3, s. 279-335
-
Journal article (peer-reviewed)abstract
- Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.
|
|
