| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
A Unified Approach for Static and Runtime Verification: Framework and Applications
- 2012
-
Ingår i: 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
-
Konferensbidrag (refereegranskat)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.
(författare)
-
Smart Contracts: A Killer Application for Deductive Source Code Verification
- 2018
-
Ingår i: Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday. - Cham : Springer International Publishing. - 9783319980478 ; , s. 1-18
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)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.
(författare)
-
Specification language for static and runtime verification of data and control properties
- 2015
-
Ingår i: 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
-
Konferensbidrag (refereegranskat)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.
(författare)
-
StaRVOOrS - Episode II: Strengthen and distribute the force
- 2016
-
Ingår i: 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
-
Konferensbidrag (refereegranskat)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.
(författare)
-
Verification of Smart Contract Business Logic: Exploiting a Java Source Code Verifier
- 2019
-
Ingår i: 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
-
Konferensbidrag (refereegranskat)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.
(författare)
-
Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- 2017
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 51:1, s. 200-265
-
Tidskriftsartikel (refereegranskat)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. |
- Alshareef, Hanaa, 1985, et al.
(författare)
-
A collaborative access control framework for online social networks
- 2020
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 114
-
Tidskriftsartikel (refereegranskat)abstract
- Most Online Social Networks allow users to set their privacy settings concerning posting information, but current implementations do not allow a fine grained enforcement in case the posted item concerns other users. In this paper we propose a new collaborative access control framework that takes into account the relation of multiple users for viewing as well as for sharing items, eventually solving conflicts in the privacy settings of the users involved. Our solution relies on two algorithms, one for viewing and another one for sharing items. We provide an evaluation of these algorithms where we demonstrate how varying some of the parameters directly influences the decision of viewing or sharing an item. Last but not least, we present a proof-of-concept implementation of our approach in an open source social network called Diaspora. (C) 2020 Elsevier Inc. All rights reserved.
|
|
| 8. |
- Alshareef, Hanaa, 1985, et al.
(författare)
-
Precise Analysis of Purpose Limitation in Data Flow Diagrams
- 2022
-
Ingår i: ACM International Conference Proceeding Series. - New York, NY, USA : ACM.
-
Konferensbidrag (refereegranskat)abstract
- Data Flow Diagrams (DFDs) are primarily used for modelling functional properties of a system. In recent work, it was shown that DFDs can be used to also model non-functional properties, such as security and privacy properties, if they are annotated with appropriate security- and privacy-related information. An important privacy principle one may wish to model in this way is purpose limitation. But previous work on privacy-aware DFDs (PA-DFDs) considers purpose limitation only superficially, without explaining how the purpose of DFD activators and flows ought to be specified, checked or inferred. In this paper, we define a rigorous formal framework for (1) annotating DFDs with purpose labels and privacy signatures, (2) checking the consistency of labels and signatures, and (3) inferring labels from signatures. We implement our theoretical framework in a proof-of concept tool consisting of a domain-specific language (DSL) for specifying privacy signatures and algorithms for checking and inferring purpose labels from such signatures. Finally, we evaluate our framework and tool through a case study based on a DFD from the privacy literature.
|
|
| 9. |
- Alshareef, Hanaa, 1985, et al.
(författare)
-
Refining Privacy-Aware Data Flow Diagrams
- 2021
-
Ingår i: 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. ; 13085, s. 121-140
-
Konferensbidrag (refereegranskat)abstract
- Privacy, like security, is a non-functional property, yet most software design tools are focused on functional aspects, using for instance Data Flow Diagrams (DFDs). In previous work, a conceptual model was introduced where DFDs were extended into so-called Privacy-Aware Data Flow Diagrams (PA-DFDs) with the aim of adding specific privacy checks to existing DFDs. An implementation to add such automatic checks has also been developed. In this paper, we define the notion of refinement for both DFDs and PA-DFDs as a special type of structure-preserving map (or graph homomorphism). We also provide three algorithms to find, check and transform refinements, and we show that the standard diagram "transform→refine/refine→transform" commutes. We have implemented our algorithms in a proof-of-concept tool called DFD Refinery , and have applied it to realistic scenarios.
|
|
| 10. |
- Alshareef, Hanaa, 1985, et al.
(författare)
-
Transforming data flow diagrams for privacy compliance
- 2021
-
Ingår i: MODELSWARD 2021 - Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development. - : SCITEPRESS - Science and Technology Publications. ; , s. 207-215
-
Konferensbidrag (refereegranskat)abstract
- Most software design tools, as for instance Data Flow Diagrams (DFDs), are focused on functional aspects and cannot thus model non-functional aspects like privacy. In this paper, we provide an explicit algorithm and a proof-of-concept implementation to transform DFDs into so-called Privacy-Aware Data Flow Diagrams (PA-DFDs). Our tool systematically inserts privacy checks to a DFD, generating a PA-DFD. We apply our approach to two realistic applications from the construction and online retail sectors.
|
|
