A formal model for an ideal CFI

Sepehr Minagar, Balasubramaniam Srinivasan, Phu Dung Le

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-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 languageEnglish
    Title of host publicationInformation Security Practice and Experience
    Subtitle of host publication13th International Conference, ISPEC 2017, Melbourne, VIC, Australia, December 13-15, 2017, Proceedings
    EditorsJoseph K. Liu, Pierangela Samarati
    Place of PublicationCham Switzerland
    PublisherSpringer
    Pages707-726
    Number of pages20
    ISBN (Electronic)9783319723594
    ISBN (Print)9783319723587
    DOIs
    Publication statusPublished - 2017
    EventInformation Security Practice and Experience Conference 2017 - Deakin Downtown, Melbourne, Australia
    Duration: 13 Dec 201715 Dec 2017
    Conference number: 13th
    http://nsclab.org/ispec2017/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10701
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    ConferenceInformation Security Practice and Experience Conference 2017
    Abbreviated titleISPEC 2017
    CountryAustralia
    CityMelbourne
    Period13/12/1715/12/17
    Internet address

    Keywords

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

    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). Cham Switzerland: 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",

    }

    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, 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 proceedingConference PaperResearchpeer-review

    TY - GEN

    T1 - A formal model for an ideal CFI

    AU - Minagar, Sepehr

    AU - Srinivasan, Balasubramaniam

    AU - Le, Phu Dung

    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

    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

    ER -

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