Current browse context:
cs.PL
Change to browse by:
References & Citations
Computer Science > Programming Languages
Title: Compositional Vulnerability Detection with Insecurity Separation Logic (Extended Version)
(Submitted on 12 Jul 2021 (v1), last revised 21 Aug 2023 (this version, v6))
Abstract: Memory-safety issues and information leakage are known to be depressingly common. We consider the compositional static detection of these kinds of vulnerabilities in first-order C-like programs. Indeed the latter are relational hyper-safety violations, comparing pairs of program executions, making them more challenging to detect than the former, which require reasoning only over individual executions. Existing symbolic leakage detection methods treat only non-interactive programs, avoiding the challenges of nondeterminism. Also, being whole-program analyses they cannot be applied one-function-at-a-time, thereby ruling out incremental analysis. We remedy these shortcomings by presenting Insecurity Separation Logic (InsecSL), an under-approximate relational program logic for soundly detecting information leakage and memory-safety issues in interactive programs. Importantly, InsecSL reasons about pairs of executions, and so is relational, but purposefully resembles the non-relational Incorrectness Separation Logic (ISL) that is already automated in the Infer tool. We show how InsecSL can be automated by bi-abduction based symbolic execution, and we evaluate two implementations of this idea (one based on Infer) on 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.