A formal model for an ideal CFI

Sepehr Minagar; Balasubramaniam Srinivasan; Phu Dung Le

doi:10.1007/978-3-319-72359-4_44

A formal model for an ideal CFI

Sepehr Minagar, Balasubramaniam Srinivasan, Phu Dung Le

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

Abstract

We provide a formal model to achieve a fully precise dynamic protection of the flow of execution against control flow hijacking attacks. In more than a decade since the original Control Flow Integrity the focus of all of the proposed work in the literature has been on practical implementation of CFI. This however due to the restriction that the classic CFI poses on function return has led to the solutions that relax and bend the rules used in the proof of the original work. Some of these solutions has been shown to be completely insecure and others are hard to prove using formal methods. We use Propositional Dynamic Logic that combines actions and their consequences in a formal system which allows us to clearly express the required pre and post conditions to prevent a class of exploitation. We prove the correctness of our scheme for an abstract machine as a model of modern processors.

Original language	English
Title of host publication	Information Security Practice and Experience
Subtitle of host publication	13th International Conference, ISPEC 2017, Melbourne, VIC, Australia, December 13-15, 2017, Proceedings
Editors	Joseph K. Liu, Pierangela Samarati
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	707-726
Number of pages	20
ISBN (Electronic)	9783319723594
ISBN (Print)	9783319723587
DOIs	https://doi.org/10.1007/978-3-319-72359-4_44
Publication status	Published - 2017
Event	Information Security Practice and Experience Conference 2017 - Deakin Downtown, Melbourne, Australia Duration: 13 Dec 2017 → 15 Dec 2017 Conference number: 13th http://nsclab.org/ispec2017/ (Website) https://link.springer.com/book/10.1007/978-3-319-72359-4 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10701
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Information Security Practice and Experience Conference 2017
Abbreviated title	ISPEC 2017
Country/Territory	Australia
City	Melbourne
Period	13/12/17 → 15/12/17
Internet address	http://nsclab.org/ispec2017/ (Website) https://link.springer.com/book/10.1007/978-3-319-72359-4 (Proceedings)

Keywords

Context-sensitive CFI
Dynamic control flow integrity
Formal security model
Malicious code execution prevention

Access to Document

10.1007/978-3-319-72359-4_44

Cite this

Minagar, S., Srinivasan, B., & Le, P. D. (2017). A formal model for an ideal CFI. In J. K. Liu, & P. Samarati (Eds.), Information Security Practice and Experience: 13th International Conference, ISPEC 2017, Melbourne, VIC, Australia, December 13-15, 2017, Proceedings (pp. 707-726). (Lecture Notes in Computer Science; Vol. 10701). Springer. https://doi.org/10.1007/978-3-319-72359-4_44

Minagar, Sepehr ; Srinivasan, Balasubramaniam ; Le, Phu Dung. / A formal model for an ideal CFI. Information Security Practice and Experience: 13th International Conference, ISPEC 2017, Melbourne, VIC, Australia, December 13-15, 2017, Proceedings. editor / Joseph K. Liu ; Pierangela Samarati. Cham Switzerland : Springer, 2017. pp. 707-726 (Lecture Notes in Computer Science).

@inproceedings{27882c9e714b4c5685312d5cded09c0b,

title = "A formal model for an ideal CFI",

abstract = "We provide a formal model to achieve a fully precise dynamic protection of the flow of execution against control flow hijacking attacks. In more than a decade since the original Control Flow Integrity the focus of all of the proposed work in the literature has been on practical implementation of CFI. This however due to the restriction that the classic CFI poses on function return has led to the solutions that relax and bend the rules used in the proof of the original work. Some of these solutions has been shown to be completely insecure and others are hard to prove using formal methods. We use Propositional Dynamic Logic that combines actions and their consequences in a formal system which allows us to clearly express the required pre and post conditions to prevent a class of exploitation. We prove the correctness of our scheme for an abstract machine as a model of modern processors.",

keywords = "Context-sensitive CFI, Dynamic control flow integrity, Formal security model, Malicious code execution prevention",

author = "Sepehr Minagar and Balasubramaniam Srinivasan and Le, {Phu Dung}",

year = "2017",

doi = "10.1007/978-3-319-72359-4_44",

language = "English",

isbn = "9783319723587",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "707--726",

editor = "Liu, {Joseph K.} and Pierangela Samarati",

booktitle = "Information Security Practice and Experience",

note = "Information Security Practice and Experience Conference 2017, ISPEC 2017 ; Conference date: 13-12-2017 Through 15-12-2017",

url = "http://nsclab.org/ispec2017/, https://link.springer.com/book/10.1007/978-3-319-72359-4",

}

Minagar, S, Srinivasan, B & Le, PD 2017, A formal model for an ideal CFI. in JK Liu & P Samarati (eds), Information Security Practice and Experience: 13th International Conference, ISPEC 2017, Melbourne, VIC, Australia, December 13-15, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10701, Springer, Cham Switzerland, pp. 707-726, Information Security Practice and Experience Conference 2017, Melbourne, Victoria, Australia, 13/12/17. https://doi.org/10.1007/978-3-319-72359-4_44

A formal model for an ideal CFI. / Minagar, Sepehr; Srinivasan, Balasubramaniam; Le, Phu Dung.
Information Security Practice and Experience: 13th International Conference, ISPEC 2017, Melbourne, VIC, Australia, December 13-15, 2017, Proceedings. ed. / Joseph K. Liu; Pierangela Samarati. Cham Switzerland: Springer, 2017. p. 707-726 (Lecture Notes in Computer Science; Vol. 10701).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - A formal model for an ideal CFI

AU - Minagar, Sepehr

AU - Srinivasan, Balasubramaniam

AU - Le, Phu Dung

N1 - Conference code: 13th

PY - 2017

Y1 - 2017

N2 - We provide a formal model to achieve a fully precise dynamic protection of the flow of execution against control flow hijacking attacks. In more than a decade since the original Control Flow Integrity the focus of all of the proposed work in the literature has been on practical implementation of CFI. This however due to the restriction that the classic CFI poses on function return has led to the solutions that relax and bend the rules used in the proof of the original work. Some of these solutions has been shown to be completely insecure and others are hard to prove using formal methods. We use Propositional Dynamic Logic that combines actions and their consequences in a formal system which allows us to clearly express the required pre and post conditions to prevent a class of exploitation. We prove the correctness of our scheme for an abstract machine as a model of modern processors.

AB - We provide a formal model to achieve a fully precise dynamic protection of the flow of execution against control flow hijacking attacks. In more than a decade since the original Control Flow Integrity the focus of all of the proposed work in the literature has been on practical implementation of CFI. This however due to the restriction that the classic CFI poses on function return has led to the solutions that relax and bend the rules used in the proof of the original work. Some of these solutions has been shown to be completely insecure and others are hard to prove using formal methods. We use Propositional Dynamic Logic that combines actions and their consequences in a formal system which allows us to clearly express the required pre and post conditions to prevent a class of exploitation. We prove the correctness of our scheme for an abstract machine as a model of modern processors.

KW - Context-sensitive CFI

KW - Dynamic control flow integrity

KW - Formal security model

KW - Malicious code execution prevention

UR - http://www.scopus.com/inward/record.url?scp=85038081407&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-72359-4_44

DO - 10.1007/978-3-319-72359-4_44

M3 - Conference Paper

AN - SCOPUS:85038081407

SN - 9783319723587

T3 - Lecture Notes in Computer Science

SP - 707

EP - 726

BT - Information Security Practice and Experience

A2 - Liu, Joseph K.

A2 - Samarati, Pierangela

PB - Springer

CY - Cham Switzerland

T2 - Information Security Practice and Experience Conference 2017

Y2 - 13 December 2017 through 15 December 2017

ER -

A formal model for an ideal CFI

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Cite this