A formal model for an ideal CFI

Sepehr Minagar, Balasubramaniam Srinivasan, Phu Dung Le

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review


    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
    Number of pages20
    ISBN (Electronic)9783319723594
    ISBN (Print)9783319723587
    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/ (Website)
    https://link.springer.com/book/10.1007/978-3-319-72359-4 (Proceedings)

    Publication series

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


    ConferenceInformation Security Practice and Experience Conference 2017
    Abbreviated titleISPEC 2017
    Internet address


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

    Cite this