Safe Pointers in SPARK 2014

TL;DR

This paper introduces a static alias analysis for SPARK 2014 that enables safe pointer usage, inspired by Rust's borrow-checker, improving formal verification capabilities for Ada-based software.

Contribution

It extends SPARK with pointer support using a novel static alias analysis inspired by Rust, with formal soundness proof and practical implementation in GNAT.

Findings

Successfully integrated pointer support into SPARK with minor code changes.

The analysis enforces safe aliasing principles, proven sound through formal methods.

Implemented in GNAT and tested on real-world examples, showing practical viability.

Abstract

In the context of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-defined subset of the Ada language, intended for formal verification of mission-critical software. Our solution is based on static alias analysis inspired by Rust's borrow-checker and affine types, and enforces the Concurrent Read, Exclusive Write principle. This analysis has been implemented in the GNAT Ada compiler and tested against a number of challenging examples including parts of real-life applications. Our tests show that only minor changes in the source code are required to fit the idiomatic Ada code into SPARK extended with pointers, which is a significant improvement upon the previous state of the art. The proposed extension has been approved by the Language Design Committee for SPARK for inclusion in a future version of SPARK, and is being discussed by the Ada Rapporteur Group for inclusion in the next version of Ada. In the report, we give a formal presentation of the analysis rules for a miniature version of SPARK and prove their soundness. We discuss the implementation and the case studies, and compare our solution with Rust.