We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.PL

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Compositional Vulnerability Detection with Insecurity Separation Logic

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. Existing methods often treat one type of vulnerability (e.g. memory-safety) but not the other (e.g. information leakage). Indeed the latter are hyper-safety violations, making them more challenging to detect than the former. Existing leakage detection methods like Relational Symbolic Execution treat only non-interactive programs, avoiding the challenges raised by nondeterminism for reasoning about information leakage. Their implementations also do not treat non-trivial leakage policies like value-dependent classification, which are becoming increasingly common. Finally, being whole-program analyses they cannot be applied compositionally -- to deduce the presence of vulnerabilities in a program by analysing each of its parts -- thereby ruling out the possibility of incremental analysis.
In this paper 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. We show how InsecSL can be soundly automated by bi-abduction based symbolic execution. Based on this, we design and implement a top-down, contextual, compositional, inter-procedural analysis for vulnerability detection. We implement our approach in a proof-of-concept tool, Underflow, for analysing C programs, which we demonstrate by applying it to various case studies.
Subjects: Programming Languages (cs.PL); Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)
Cite as: arXiv:2107.05225 [cs.PL]
  (or arXiv:2107.05225v4 [cs.PL] for this version)

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)

Link back to: arXiv, form interface, contact.