Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/73739
Title: | Residual-based combination of static and runtime verification |
Authors: | Azzopardi, Shaun (2019) |
Keywords: | Computer software -- Verification Programming languages (Electronic computers) Formal methods (Computer science) Computer logic |
Issue Date: | 2019 |
Citation: | Azzopardi, S. (2019). Residual-based combination of static and runtime verification (Doctoral dissertation). |
Abstract: | While verification techniques attempt to solve the problem of checking that a program satisfies a property they can fail and give an indeterminate verdict. In a survey of literature we identify approaches that improve this by allowing a verification technique to produce a new proof obligation by either transforming a property and/or transforming a program. Here we choose to focus on techniques that transform a property. To reason about these we present an abstract formal framework that characterises properties in terms of the programs that satisfy them. In turn we are able to characterise a residual property that is equivalent to the original property for the program under verification. We instantiate this approach for both state- and event-based properties, showing how the conjunction of properties can be wielded to produce effective residual properties to reduce the verification effort for subsequent techniques. We validate further this approach for state-based properties in the context of industrial project involving a payments ecosystem and untrusted client applications, where a enforced model of behaviour allows us to verify or partially evaluate at pre-deployment certain regulations specified as universally quantified propositions. Our main contribution is an approach for the combination of static and runtime verification for automata-based properties. Existing such approaches focus on the reduction of instrumentation of a program, while we present an approach to the reduction of structural elements of a property. We focus on dynamic event automata (DEA) as event-based properties that monitor both the program control-flow and the program data-state. We give an intraprocedural approach to analysing a property against a program. This allows us to collect knowledge about the behaviour of each procedure individually (ignoring possible outside behaviour) to produce a residual of the whole-program. The algorithm can easily be adapted to the interprocedural case. Moreover, by adding an assertion propagation algorithm and the use of an SMT solver we show how this can be optimised by pruning the possible behaviour and evaluating property guards. We validated this approach on both Java programs and Solidity smart contracts, showing moderate overhead improvements but significant progress in reducing the property. |
Description: | PH.D.COMPUTER SCIENCE |
URI: | https://www.um.edu.mt/library/oar/handle/123456789/73739 |
Appears in Collections: | Dissertations - FacICT - 2019 Dissertations - FacICTCS - 2019 |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
19PHDIT002 - Shaun Azzopardi.pdf | 1.79 MB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.