The Tome of Secure Compilation: Fully Abstract Compilation to Protected Modules Architectures

1 Summary The goal of this research project is to enhance the security of networked, embedded computing devices. A networked, embeddedcomputing device consists of a hardware part and a software part; both components play an essential role in the overall security of a device. The software builds on hardware low level security blocks to provide higher-level guarantees such as process isolation, secure communication, or even application-specific security guarantees such as non- repudiation of transactions. On the general-purposenbsp;side, hardware soon became de factonbsp;and research on system security treated the underlying hardware as a given. System security was achieved in software,building on the standard hardware building blocks. Now that embedded devices are becoming more and more networked, and hence face new security threats, it is again important to look at the interaction between hardware security features and software security. Many embedded platforms lackthe standard security features (such as privilege levels or advanced memory management units) present in high-end processors, and extending such hardware platform with custom instructions or coprocessors to achieve betternbsp;guarantees for the overall system is a sensible and feasible path. So far there is little fundamental research on what the advantages, limits and trade-offs are of co-designing hardware and software for security purposes. This project aims to fill this void. The project will build a model of adaptive embedded networked systems that makes explicit the division between what is implemented in hardware and what insoftware. It will analyze the attacks that are possible against the hardware part and against the software part.nbsp;insights gained by this analysis will drive the design of new softwarenbsp;features. Finally this project will aim to fillingnbsp;void in hardware/software co-designfoundations fornbsp;systems. Additional challenges and opportunities arise for networked embedded systems. Thenbsp;facilitiesoffered by networked devices give rise to new threats (such as for instance increased attack surface), but also to new security enforcement techniques, as devices may now rely on trusted third partiesnbsp;overthe network. Anothernbsp;that will be explored is adaptivity: most IT systems have static defences, while biological defences are adaptive: increasing security may present a high overhead and therefore an optimal security system can adjust itself to the threat environment and the context. As networked embedded systems are typically deployed in not completely known and often varying environments, they need to be adaptable to the changing context in terms of the functionality offered, changing security requirements, and due to new code dynamically added to the device. It is clear of coursenbsp;care is needed when adding adaptivity, asthis opens the door to new attack vectors. 2 Planning The project will involve the following three tasks. 2.1nbsp;nbsp;System model and requirements What does it mean for a networked embedded device to be secure when adapting to the needs of a dynamically changing environment? To answer this question, two issuesnbsp;to be addressed. First, one needs to identifynbsp;the security requirements of the various stakeholders are in typical applications of networked embedded devices [5]. And second, one needs a model of a networked embedded device that has sufficient detail to assess whether hardware/software based countermeasure implementations provide sufficient assurance that the device will live up to the stakeholders requirements [6]. This phase of the research will produce the following outcomes: • a model of networked embeddednbsp;devices • a formalism for specifying overall system security policiesnbsp;such devices • a number of relevant example policies, in particular policies that are challenging to enforce using state-of-the-art techniques • the definition of the class of attacks relevant against hardware and software components At present, a survey of attacks on networked embedded devicesnbsp;proposed counter- measures has been compiled. 2.2nbsp; Software security building blocks After a firstnbsp;of foundation laying, the project will focus on basic research on software security techniques. Such techniques come in two guises: a first class of techniques tries to ensure that software behavior complies with a predefined policy [8] (stack canaries [4], execu- tion monitors [8] and soforth), and a second class of techniques tries to protect the integrityor confidentiality of the softwarenbsp;[1] (software obfuscation [3], software attestation [7] and white box cryptography [2]). The project will study and improve techniques from both classes. The research is meant to provide the following outcomes: nbsp;Static(and hybrid) checking approaches of various degrees of automation (program analyzes, type systems, Hoare logics) for enforcing security mechanisms • The design, implementation and validation of softwarenbsp;techniques to enforce the integrity and confidentiality of software. 2.3nbsp; Hardware/softwarenbsp;for security Finallynbsp;research project addresses the ambitious researchnbsp;howshould security responsibilities be distributed over hardware and software? Traditionally, hardware/software co-design, i.e. defining the platformnbsp;the code that will run on it at the same time, is done to combine performance with flexibility. The fundamental problem with hardware/software co-design for security is that there is no clear metric to measure the overall security im- provement. (Contrary to a throughput increase or a power reduction, which can be clearly measured.) The modelsnbsp;from the earlynbsp;of this project will be crucial for this. The expected outcome of this final phase includes the design of several useful and novel in- stances of hardware/software co-design for security, and fundamental new insights in hardware- assisted software protectionmechanisms. References [1] Jan Cappaert, Brecht Wyseur, and Bart Preneel. Software security techniques. Technical report, Katholieke Universiteit Leuven, 2004. [2] Stanley Chow, Philip A. Eisen, Harold Johnson, and Paul C. vannbsp;White-box cryptography and an aes implementation. In Revised Papers from the 9th Annual Inter-nbsp;Workshop on Selected Areas in Cryptography, SAC ’02, pages 250–270, London, UK, 2003. Springer-Verlag. [3] Christian S. Collberg andnbsp;Thomborson.Watermarking, tamper-proofing, and ob- fuscation: tools for software protection. IEEE Trans. Softw. Eng., 28:735–746, August 2002. [4] Cigrave;edric Fournet and Andrew D. Gordon. Stacknbsp;Theory andvariants. ACM Trans. Program. Lang. Syst., 25:360–399, May 2003. [5]Seda F. Gu#776;rses and Thomas Santen. Contextualizing security goals: A method fornbsp;tilateral security requirements elicitation. InSicherheit, pagesndash;53, 2006. [6] Naeem Muhammad, Yves Vandewoude, Yolande Berbers, and Sjir van Loo. Modelling embedded eystems with AADL:A practical study. In Aleksandar Lazinica,nbsp;New Advanced Technologies, pages 247–263. INTECH, 2010. [7] George C. Necula. Proof-carrying code. In POPL, pages 106nbsp;1997. [8] Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30– 50, 2000.status: publishe