CFG construction soundness in Control-Flow integrity

Gang Tan; Trent Jaeger

doi:10.1145/3139337.3139339

CFG construction soundness in Control-Flow integrity

Gang Tan
, Trent Jaeger

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

13 Scopus citations

Abstract

Control-Flow Integrity (CFI) is an intensively studied technique for hardening software security. It enforces a Control-Flow Graph (CFG) by inlining runtime checks into target programs. Many methods have been proposed to construct the enforced CFG, with different degrees of precision and sets of assumptions. However, past CFI work has not made attempt at justifying their CFG construction soundness using formal semantics and proofs. In this paper, we formalize the CFG construction in two major CFI systems, identify their assumptions, and prove their soundness; the soundness proof shows that their computed sets of targets for indirect calls are safe over-approximations.

Original language	English (US)
Title of host publication	PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017
Publisher	Association for Computing Machinery, Inc
Pages	3-13
Number of pages	11
ISBN (Electronic)	9781450350990
DOIs	https://doi.org/10.1145/3139337.3139339
State	Published - Oct 30 2017
Event	12th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2017 - Dallas, United States Duration: Oct 30 2017 → …

Publication series

Name	PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017
Volume	2017-January

Other

Other	12th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2017
Country/Territory	United States
City	Dallas
Period	10/30/17 → …

All Science Journal Classification (ASJC) codes

Computational Theory and Mathematics
Computer Science Applications
Software

Access to Document

10.1145/3139337.3139339

Cite this

Tan, G., & Jaeger, T. (2017). CFG construction soundness in Control-Flow integrity. In PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017 (pp. 3-13). (PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017; Vol. 2017-January). Association for Computing Machinery, Inc. https://doi.org/10.1145/3139337.3139339

Tan, Gang ; Jaeger, Trent. / CFG construction soundness in Control-Flow integrity. PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017. Association for Computing Machinery, Inc, 2017. pp. 3-13 (PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017).

@inproceedings{c9cf7888ec5949a8905ac1ade69725f9,

title = "CFG construction soundness in Control-Flow integrity",

abstract = "Control-Flow Integrity (CFI) is an intensively studied technique for hardening software security. It enforces a Control-Flow Graph (CFG) by inlining runtime checks into target programs. Many methods have been proposed to construct the enforced CFG, with different degrees of precision and sets of assumptions. However, past CFI work has not made attempt at justifying their CFG construction soundness using formal semantics and proofs. In this paper, we formalize the CFG construction in two major CFI systems, identify their assumptions, and prove their soundness; the soundness proof shows that their computed sets of targets for indirect calls are safe over-approximations.",

author = "Gang Tan and Trent Jaeger",

note = "Publisher Copyright: {\textcopyright} 2017 Association for Computing Machinery.; 12th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2017 ; Conference date: 30-10-2017",

year = "2017",

month = oct,

day = "30",

doi = "10.1145/3139337.3139339",

language = "English (US)",

series = "PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017",

publisher = "Association for Computing Machinery, Inc",

pages = "3--13",

booktitle = "PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017",

}

Tan, G & Jaeger, T 2017, CFG construction soundness in Control-Flow integrity. in PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017. PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017, vol. 2017-January, Association for Computing Machinery, Inc, pp. 3-13, 12th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2017, Dallas, United States, 10/30/17. https://doi.org/10.1145/3139337.3139339

CFG construction soundness in Control-Flow integrity. / Tan, Gang; Jaeger, Trent.
PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017. Association for Computing Machinery, Inc, 2017. p. 3-13 (PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017; Vol. 2017-January).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - CFG construction soundness in Control-Flow integrity

AU - Tan, Gang

AU - Jaeger, Trent

PY - 2017/10/30

Y1 - 2017/10/30

N2 - Control-Flow Integrity (CFI) is an intensively studied technique for hardening software security. It enforces a Control-Flow Graph (CFG) by inlining runtime checks into target programs. Many methods have been proposed to construct the enforced CFG, with different degrees of precision and sets of assumptions. However, past CFI work has not made attempt at justifying their CFG construction soundness using formal semantics and proofs. In this paper, we formalize the CFG construction in two major CFI systems, identify their assumptions, and prove their soundness; the soundness proof shows that their computed sets of targets for indirect calls are safe over-approximations.

AB - Control-Flow Integrity (CFI) is an intensively studied technique for hardening software security. It enforces a Control-Flow Graph (CFG) by inlining runtime checks into target programs. Many methods have been proposed to construct the enforced CFG, with different degrees of precision and sets of assumptions. However, past CFI work has not made attempt at justifying their CFG construction soundness using formal semantics and proofs. In this paper, we formalize the CFG construction in two major CFI systems, identify their assumptions, and prove their soundness; the soundness proof shows that their computed sets of targets for indirect calls are safe over-approximations.

UR - https://www.scopus.com/pages/publications/85043357015

UR - https://www.scopus.com/pages/publications/85043357015#tab=citedBy

U2 - 10.1145/3139337.3139339

DO - 10.1145/3139337.3139339

M3 - Conference contribution

AN - SCOPUS:85043357015

T3 - PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017

SP - 3

EP - 13

BT - PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017

PB - Association for Computing Machinery, Inc

T2 - 12th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, PLAS 2017

Y2 - 30 October 2017

ER -

Tan G, Jaeger T. CFG construction soundness in Control-Flow integrity. In PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017. Association for Computing Machinery, Inc. 2017. p. 3-13. (PLAS 2017 - Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, co-located with CCS 2017). doi: 10.1145/3139337.3139339

CFG construction soundness in Control-Flow integrity

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this