Gillian, Part II: Real-World Verification for JavaScript and C

Authors

  • Petar Maksimovic
  • Sacha-Élie Ayoun
  • José Fragoso Santos
  • Philippa Gardner

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, specifically designing common abstractions used for both verification tasks, and find two bugs in the JavaScript and three bugs in the C implementation.

Venue

Proceedings of the 33rd Computer Aided Verification International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Part II, pp. 827–850

Publication Date

2021

Identifiers

Source Materials