Authentic Execution of Distributed Event-Driven Applications with a Small TCBJob Noorman,
Jan
Tobias Mühlberg,
and Frank Piessens This page contains suplementary material for STM 2017 submission 4: "Authentic Execution of Distributed Event-Driven Applications with a Small TCB" Abstract. This paper presents an approach to provide strong assurance of the secure execution of distributed event-driven applications on shared infrastructures, while relying on a small Trusted Computing Base. We build upon and extend security primitives provided by a Protected Module Architecture (PMA) to guarantee authenticity and integrity properties of applications, and to secure control of input and output devices used by these applications. More specifically, we want to guarantee that if an output is produced by the application, it was allowed to be produced by the application's source code. We present a prototype implementation as an extension of Sancus, a light-weight embedded PMA that extends the TI MSP430 CPU. Our evaluation of the security and performance aspects of our approach and the prototype show that PMA together with our programming model form a basis for powerful security architectures for dependable systems in domains such as Industrial Control Systems, the Internet of Things or Wireless Sensor Networks. Paper: paper.pdf Formal Definition and Proof of Security Properties. This document can be seen as an extended appendix to the paper, in which we focus on defining a simple reactive programming language for our architecture, the formal semantics of that programming language, and the formal definition and proof of the security properties of our approach. We further provide background information on our performance evaluation and a more complete discussion of the related work, as the version in the paper is rather brief: secargument.pdf Implementation and Demonstration Scenario. Below we provide the source code for the paprking sensors demonstration scenario that we discuss in the paper. To compile the code you will need the Sancus tools and MSP430-GCC installed on your system. Note that the demo scenario cannot be executed in the Sancus simulator (simulating the CPU behaviour at the gate level, the Sancus simulator is too slow to perform network operations) but must be run on an FPGA programmed with the Sancus core. In our experiments we used a Spartan 6 FPGA: parking-sensors.tar.gz (2.3 KiB) For convenience we provide quick links to the source code and the deployment descriptor, as described in the paper. Drivers, scheduler and module loader are part of recent Sancus distributions.
Jan Tobias Mühlberg, Wed, 23 Aug 2017 17:23:56 +0200 | ||||||||||||||||||||||||||||