Publications
122 results found
Karmios N, Ayoun S-É, Gardner P, 2023, Symbolic debugging with Gillian, DEBT '23: 1st ACM International Workshop on Future Debugging Techniques, Publisher: ACM, Pages: 1-2
Software debugging for concrete execution enjoys a mature suite of tools, but debugging symbolic execution is still in its infancy. It carries unique challenges, as a single state can lead to multiple branches representing different sets of conditions, and symbolic states must be 'matched' against logical conditions. Some of today’s otherwise mature symbolic-execution tools still rely on plain-text log files for debugging, which provide no good overview of the execution process and can quickly become overwhelming. We introduce a debugger for Gillian’s verification mode---complete with a custom interface---and ponder the potential for this interface and the protocol behind it to be used outside of Gillian.
Maksimovic P, Cronjäger C, Loow A, et al., 2023, Exact separation logic: towards bridging the gap between verification and bug-finding, ECOOP 2023, Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 19:1-19:27, ISSN: 1868-8969
Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised.We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.
Rao X, Georges AL, Legoupil M, et al., 2023, Iris-Wasm: robust and modular verification of WebAssembly programs, PLDI 2023, Publisher: Association for Computing Machinery (ACM), Pages: 1096-1120, ISSN: 2475-1421
WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher- order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.
D'Osualdo E, Sutherland J, Farzan A, et al., 2021, TaDA Live: compositional reasoning for termination of fine-grained concurrent programs, ACM Transactions on Programming Languages and Systems, Vol: 43, ISSN: 0164-0925
We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients which use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants, and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.
D'Osualdo E, Sutherland J, Farzan A, et al., 2021, TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs, Publisher: ASSOC COMPUTING MACHINERY
- Author Web Link
- Cite
- Citations: 2
Watt C, Rao X, Pichon-Pharabod J, et al., 2021, Two mechanisations of WebAssembly 1.0, 24th international symposium of Formal Methods (FM21), Publisher: Springer Verlag, Pages: 61-79, ISSN: 0302-9743
WebAssembly (Wasm) is a new bytecode language supportedby all major Web browsers, designed primarily to be an efficient com-pilation target for low-level languages such as C/C++ and Rust. It isunusual in that it is officially specified through a formal semantics. Aninitial draft specification was published in 2017 [14], with an associatedmechanised specification in Isabelle/HOL published by Watt that foundbugs in the original specification, fixed before its publication [37].The first official W3C standard, WebAssembly 1.0, was published in2019 [45]. Building on Watt’s original mechanisation, we introduce twomechanised specifications of the WebAssembly 1.0 semantics, writtenin different theorem provers: WasmCert-Isabelle and WasmCert-Coq.Wasm’s compact design and official formal semantics enable our mecha-nisations to be particularly complete and close to the published languagestandard. We present a high-level description of the language’s updatedtype soundness result, referencing both mechanisations. We also describethe current state of the mechanisation of language features not previouslysupported: WasmCert-Isabelle includes a verified executable definitionof the instantiation phase as part of an executable verified interpreter;WasmCert-Coq includes executable parsing and numeric definitions ason-going work towards a more ambitious end-to-end verified interpreterwhich does not require an OCaml harness like WasmCert-Isabelle.
Maksimovic P, Fragoso Santos J, Ayoun SE, et al., 2021, Gillian, Part II: real-world verification for JavaScript and C, 33rd International Conference on Computer-Aided Verification, (CAV 2021), Publisher: Springer Verlag, Pages: 827-850, ISSN: 0302-9743
We introduce verification based on separation logic to Gillian, a multi-language platform for the development of symbolic analysis tools which is parametric on the memory model of the target language. Our work develops a methodology for constructing compositional memory models for Gillian, leading to a unified presentation of the JavaScript and C memory models. We verify the JavaScript and C implementations of the AWS Encryption SDK message header deserialisation module, specificallydesigning common abstractions used for both verification tasks, and find two bugs in the JavaScript and three bugs in the C implementation.
Sampaio G, Fragoso Santos J, Maksimovic P, et al., 2020, A trusted infrastructure for symbolic analysis of event-driven web applications, 34th European Conference on Object-Oriented Programming (ECOOP 2020), Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 28:1-28:29, ISSN: 1868-8969
We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applica-tions. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UIEvents, JavaScript Promises and the JavaScriptasync/awaitAPIs, all underpinned by a simpleCore Event Semantics which is sufficiently expressive to describe the event models underlying theseAPIs. Our reference implementations are trustworthy in that three follow the appropriate standardsline-by-line and all are thoroughly tested against the official test-suites, passing all the applicabletests. Using the Core Event Semantics and the reference implementations, we develop JaVerT.Click,a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScriptprograms that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click byproving both the presence and absence of bugs in real-world JavaScript code.
Fragoso Santos J, Maksimovic P, Ayoun S-E, et al., 2020, Gillian, Part I: a multi-language platform for symbolic execution, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020), Publisher: Association for Computing Machinery, Pages: 927-942
We introduce Gillian, a platform for developing symbolic analysis tools for programming languages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is parametric on the memory model of the target language. We give a formal description of the symbolic analysis and a modular implementation that closely follows this descrip- tion. We prove a parametric soundness result, introducing restriction on abstract states, which generalises path condi- tions used in classical symbolic execution. We instantiate Gillian to obtain trusted symbolic testing tools for JavaScript and C, and use these tools to find bugs in real-world code, thus demonstrating the viability of our parametric approach.
Xiong S, Cerone A, Raad A, et al., 2020, Data Consistency in Transactional Storage Systems: a Centralised Approach, 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '20)
Xiong S, Cerone A, Raad A, et al., 2019, Data consistency in transactional storage systems: a centralised approach., Publisher: arXiv
We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. We provide operational definitions of consistency models for our key-value stores which are shown to be equivalent to the well-known declarative definitions of consistency model for execution graphs. We explore two immediate applications of our semantics: specific protocols of geo-replicated databases (e.g. COPS) and partitioned databases (e.g. Clock-SI) can be shown to be correct for a specific consistency model by embedding them in our centralised semantics; programs can be directly shown to have invariant properties such as robustness results against a weak consistency model.
Watt C, Maksimovic P, Neelakantan R K, et al., 2019, A program logic for first-order encapsulated WebAssembly, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)., Publisher: Leibniz-Zentrum für Informatik, Dagstuhl Publishing, ISSN: 1868-8969
We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. Wedesign a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strongguarantees given by WebAssembly’s type system, and show how to adapt the standard separationlogic triple and proof rules in a principled way to capture WebAssembly’s uncommon structuredcontrol flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, givingabstract specifications independent of the underlying implementation. We mechanise Wasm Logicand its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formaliseand fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, upto transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the firstprogram logic for WebAssembly, and represents a first step towards the creation of static analysistools for WebAssembly.
Gardner P, Smith GD, Wright AD, 2019, Resource Reasoning about Mashups, Verified Software: Theories, Tools and Experiments, VSTTE’10, VS-Theory workhsop
Fragoso Santos J, Maksimovic P, Cunha Sampaio G, et al., 2019, JaVerT 2.0: compositional symbolic execution for JavaScript, ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery, Pages: 66:1-66:31, ISSN: 2475-1421
We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.
Bodin M, Gardner P, Jensen T, et al., 2019, Skeletal semantics and their interpretations, ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ), Publisher: Association for Computing Machinery, Pages: 44:1-44:31, ISSN: 2475-1421
The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.
Gardner P, 2018, JaVerT: JavaScript verification and testing framework, 20th International Symposium on Principles and Practice of Declarative Programming (PPDP), Publisher: Association Company Machinery
Faustino Fragoso Femenin Dos Santos J, Maksimovic P, Grohens T, et al., 2018, Symbolic execution for JavaScript, 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Publisher: ACM
We present a framework for trustworthy symbolic execution of JavaScripts programs, whose aim is to assist developers in the testing of their code: the developer writes symbolic tests for which the framework provides concrete counter-models. We create the framework following a new, general methodology for designing compositional program analyses for dynamic languages. We prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to whole-program symbolic testing of real-world JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs.
Ntzik G, da Rocha Pinto P, Sutherland JHJ, et al., 2018, A concurrent specification of POSIX file systems, 32nd European Conference on Object-Oriented Programming (ECOOP 2018), Publisher: ECOOP, Pages: 1-28
POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard’s description of concurrent behaviour is nsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files.
Dinsdale-Young TW, da Rocha Pinto P, Gardner PA, 2018, A perspective on specifying and verifying concurrent modules, Journal of Logical and Algebraic Methods in Programming, Vol: 98, Pages: 1-25, ISSN: 2352-2208
The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.
Faustino Fragoso Femenin Dos Santos J, Maksimovic P, Naudziuniene D, et al., 2018, JaVerT: JavaScript verification toolchain, ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery, ISSN: 2475-1421
The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. To specify JavaScript programs, we design abstractions that capture its key heap structures (for example, prototype chains and function closures), allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals. To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript; JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic; and verified axiomatic specifications of the JavaScript internal functions. Using JaVerT, we verify functional correctness properties of: data-structure libraries (key-value map, priority queue) written in an object-oriented style; operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures; and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger, more complex code using JaVerT is feasible.
Ntzik G, da Rocha Pinto PM, Sutherland J, et al., 2018, A concurrent speci cation of POSIX file systems technical report, Departmental Technical Report: 18/3, Publisher: Department of Computing, Imperial College London
Gardner P, 2017, Verified trustworthy software systems, Philosophical Transactions of the Royal Society A. Mathematical, Physical and Engineering Sciences, Vol: 375, ISSN: 1364-503X
Faustino Fragoso Femenin Dos Santos J, Gardner P, Naudziuniene D, et al., 2017, Towards logic-based verification of javascript programs, 26th Conference on Automated Deduction (CADE 26), Publisher: Springer Verlag, Pages: 8-25, ISSN: 0302-9743
In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe JaVerT, our semiautomatic toolchain for JavaScript verification.
Xiong S, da Rocha Pinto P, Ntzik G, et al., 2017, Abstract specifications for concurrent maps, 26th European Symposium on Programming, ESOP 2017, Publisher: Springer Berlin Heidelberg, Pages: 964-990
Despite recent advances in reasoning about concurrent datastructure libraries, the largest implementations injava.util.concurrenthave yet to be verified. The key issue lies in the development of modularspecifications, which provide clear logical boundaries between clients andimplementations. A solution is to use recent advances in fine-grained con-currency reasoning, in particular the introduction ofabstract atomicityto concurrent separation logic reasoning. We present two specificationsof concurrent maps, both providing the clear boundaries we seek. Weshow that these specifications are equivalent, in that they can be builtfrom each other. We show how we can verify client programs, such as aconcurrent set and a producer-consumer client. We also give a substan-tial first proof that the main operations ofConcurrentSkipListMapinjava.util.concurrentsatisfy the map specification. This work demon-strates that we now have the technology to verify the largest implemen-tations injava.util.concurrent.
Dinsdale-Young T, da Rocha Pinto P, Just Andersen K, et al., 2017, Caper: automatic verification for fine-grained concurrency, 26th European Symposium on Programming, ESOP 2017, Publisher: Springer Verlag, Pages: 420-447, ISSN: 0302-9743
Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reasoning in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.
Xiong S, da Rocha Pinto P, Ntzik G, et al., 2017, Abstract specifications for concurrent maps (extended version), Departmental Technical Report: 17/1, Publisher: Department of Computing, Imperial College London, 2017/1
Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.
Raad A, Fragoso Santos J, Gardner P, 2016, DOM: Specification and Client Reasoning, Asian Symposium on Programming Languages and Systems, Publisher: Springer Verlag, Pages: 401-422, ISSN: 0302-9743
We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM.
Raad A, Hobor A, Villard J, et al., 2016, Verifying concurrent graph algorithms, Asian Symposium on Programming Languages and Systems, Publisher: Springer Verlag, Pages: 314-334, ISSN: 0302-9743
We show how to verify four challenging concurrent fine-grained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction ( Open image in new window ) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.
da Rocha Pinto P, Dinsdale-Young T, Gardner PA, et al., 2016, Modular Termination Verification for Non-blocking Concurrency, 25th European Symposium on Programming, ESOP 2016, Publisher: Springer Berlin Heidelberg, Pages: 176-201, ISSN: 0302-9743
We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.
da Rocha Pinto P, Dinsdale-Young T, Gardner P, et al., 2016, Modular Termination Verification for Non-blocking Concurrency (Extended Version), Modular Termination Verification for Non-blocking Concurrency, Publisher: Department of Computing, Imperial College London, 2016/6
We present Total-TaDA, a program logic for verifying the total correctness of concurrent programs: that such programs both terminate and produce the correct result. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for non-blocking algorithms, e.g. a counter and a stack. Our specifications can express lock- and wait-freedom. More generally, they can express that one operation cannot impede the progress of another, a new non-blocking property we call non-impedance. Moreover, our approach is modular. We can verify the operations of a module independently, and build up modules on top of each other.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.