Sound symbolic execution via abstract interpretation and its application to security

DOI10.1007/978-3-031-24950-1_13zbMATH Open1529.68084arXiv2301.07783OpenAlexW4316662528MaRDI QIDQ6174402FDOQ6174402

Authors: Ignacio Tiraboschi, Tamara Rezk, Xavier Rival 

Publication date: 17 August 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Symbolic execution is a program analysis technique commonly utilized to determine whether programs violate properties and, in case violations are found, to generate inputs that can trigger them. Used in the context of security properties such as noninterference, symbolic execution is precise when looking for counterexample pairs of traces when insecure information flows are found, however it is sound only up to a bound thus it does not allow to prove the correctness of programs with executions beyond the given bound. By contrast, abstract interpretation-based static analysis guarantees soundness but generally lacks the ability to provide counterexample pairs of traces. In this paper, we propose to weave both to obtain the best of two worlds. We demonstrate this with a series of static analyses, including a static analysis called RedSoundRSE aimed at verifying noninterference. RedSoundRSE provides both semantically sound results and the ability to derive counterexample pairs of traces up to a bound. It relies on a combination of symbolic execution and abstract domains inspired by the well known notion of reduced product. We formalize RedSoundRSE and prove its soundness as well as its relative precision up to a bound. We also provide a prototype implementation of RedSoundRSE and evaluate it on a sample of challenging examples.

Full work available at URL: https://arxiv.org/abs/2301.07783

Recommendations

• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Symbolic execution based on language transformation
• Abstract non-interference
• Abstract execution
• On the nature of symbolic execution

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites Work

• Symbolic execution and program testing
• Systematic design of program transformation frameworks by abstract interpretation
• Secure information flow by self-composition
• Abstract non-interference
• On flow-sensitive security types
• Static Analysis
• Hypercollecting semantics and its application to static analysis of information flow
• Coupled relational symbolic execution for differential privacy
• Spot the difference: secure multi-execution and multiple facets
• Title not available (Why is that?)

This page was built for publication: Sound symbolic execution via abstract interpretation and its application to security

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174402)