Current browse context:
cs.PL
Change to browse by:
References & Citations
Computer Science > Programming Languages
Title: Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic
(Submitted on 12 Jul 2021 (this version), latest version 21 Aug 2023 (v6))
Abstract: We present the first compositional, incremental static analysis for detecting memory-safety and information leakage vulnerabilities in C-like programs. To do so, we develop the first under-approximate relational program logics, including Insecurity Separation Logic (InsecSL). We show how InsecSL can be automated via back-propagating symbolic execution (BPSE) to build a bottom-up, inter-procedural and incremental analysis for detecting vulnerabilities. We prove our approach sound in Isabelle/HOL and implement it in a proof-of-concept tool, Underflow, for analysing C programs, which we apply to various case studies.
Submission history
From: Toby Murray [view email][v1] Mon, 12 Jul 2021 07:11:58 GMT (99kb,D)
[v2] Mon, 13 Sep 2021 12:50:41 GMT (111kb,D)
[v3] Mon, 4 Oct 2021 03:59:16 GMT (74kb,D)
[v4] Thu, 12 May 2022 23:38:07 GMT (62kb,D)
[v5] Mon, 29 May 2023 05:38:45 GMT (29kb)
[v6] Mon, 21 Aug 2023 00:01:07 GMT (30kb)
Link back to: arXiv, form interface, contact.