Fully abstract trace semantics for low-level isolation mechanisms
2014 (English)In: Symposium on Applied Computing, SAC 2014. / [ed] Yookun Cho, Sung Y. Shin, Sang-Wook Kim, Chih-Cheng Hung, Jiman Hong, ACM Press, 2014, 1562-1569 p.Conference paper (Refereed)
Many software systems adopt isolation mechanisms of modernprocessors as software security building blocks. Reasoningabout these building blocks means reasoning aboutelaborate assembly code, which can be very complex due tothe loose structure of the code. A way to overcome this complexityis giving the code a more structured semantics. Thispaper presents one such semantics, namely a fully abstracttrace semantics, for an assembly language enhanced withprotection mechanisms of modern processors. The trace semanticsrepresents the behaviour of protected assembly codewith simple abstractions, unburdened by low-level details, atthe maximum degree of precision. Additionally, it capturesthe capabilities of attackers to protected software and simplifiesproviding a secure compiler targeting that language.
Place, publisher, year, edition, pages
ACM Press, 2014. 1562-1569 p.
IdentifiersURN: urn:nbn:se:uu:diva-237725DOI: 10.1145/2554850.2554865ISBN: 978-1-4503-2469-4OAI: oai:DiVA.org:uu-237725DiVA: diva2:768675
Symposium on Applied Computing, SAC 2014. , Gyeongju, Republic of Korea - March 24 - 28, 2014.