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 SizeFormat 
19PHDIT002 - Shaun Azzopardi.pdf1.79 MBAdobe PDFView/Open


Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.