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.
CITATION STYLE
Minagar, S., Srinivasan, B., & Le, P. D. (2017). A formal model for an ideal CFI. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10701 LNCS, pp. 707–726). Springer Verlag. https://doi.org/10.1007/978-3-319-72359-4_44
Mendeley helps you to discover research relevant for your work.