TY - GEN
T1 - CFG construction soundness in Control-Flow integrity
AU - Tan, Gang
AU - Jaeger, Trent
N1 - Funding Information:
We thank anonymous reviewers for their insightful comments, which helped us substantially improve the paper. This research is based upon work supported by US NSF grants CNS-1624126, CNS- 1408880, CCF-1624124, the Defense Advanced Research Projects Agency (DARPA) under agreement number N66001-13-2-4040, and Office of Naval Research Grant N00014-17-1-2498. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of any of the above organizations or any person connected with them.
Publisher Copyright:
© 2017 Association for Computing Machinery.
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 - http://www.scopus.com/inward/record.url?scp=85043357015&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85043357015&partnerID=8YFLogxK
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 -