Gillian, Part II: real-world verification for JavaScript and C
File(s)
Published version
Author(s)
Maksimovic, Petar
Fragoso Santos, Jose
Ayoun, Sacha Elie
Gardner, Philippa
Type
Conference Paper
Abstract
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.
Date Issued
2021-07-15
Date Acceptance
2021-04-17
Citation
Lecture Notes in Computer Science, 2021, pp.827-850
ISSN
0302-9743
Publisher
Springer Verlag
Start Page
827
End Page
850
Journal / Book Title
Lecture Notes in Computer Science
Copyright Statement
© 2021 The Author(s). Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
License URL
Sponsor
Engineering & Physical Science Research Council (E
Facebook
Identifier
https://link.springer.com/chapter/10.1007/978-3-030-81688-9_38
Grant Number
EP/R034567/1
Continuous Reasoning Call
Source
33rd International Conference on Computer-Aided Verification, (CAV 2021)
Subjects
Science & Technology
Technology
Computer Science, Hardware & Architecture
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2021-07-18
Finish Date
2021-07-24
Coverage Spatial
Virtual
Date Publish Online
2021-07-15