Trustworthy prevention of code injection in Linux on embedded devices
2015 (English)In: 20th European Symposium on Research in Computer Security, ESORICS 2015, Springer, 2015, 90-107 p.Conference paper (Refereed)Text
We present MProsper, a trustworthy system to prevent code injection in Linux on embedded devices. MProsper is a formally verified run-time monitor, which forces an untrusted Linux to obey the executable space protection policy; a memory area can be either executable or writable, but cannot be both. The executable space protection allows the MProsper’s monitor to intercept every change to the executable code performed by a user application or by the Linux kernel. On top of this infrastructure, we use standard code signing to prevent code injection. MProsper is deployed on top of the Prosper hypervisor and is implemented as an isolated guest. Thus MProsper inherits the security property verified for the hypervisor: (i) Its code and data cannot be tampered by the untrusted Linux guest and (ii) all changes to the memory layout is intercepted, thus enabling MProsper to completely mediate every operation that can violate the desired security property. The verification of the monitor has been performed using the HOL4 theorem prover and by extending the existing formal model of the hypervisor with the formal specification of the high level model of the monitor.
Place, publisher, year, edition, pages
Springer, 2015. 90-107 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9326
Codes (symbols), Embedded systems, Linux, Security of data, Security systems, Systems analysis, Embedded device, Executable codes, High-level modeling, Protection policy, Security properties, Standard codes, Theorem provers, Trustworthy systems, Computer operating systems
IdentifiersURN: urn:nbn:se:kth:diva-181591DOI: 10.1007/978-3-319-24174-6_5ISI: 000374478000005ScopusID: 2-s2.0-84951274986ISBN: 9783319241739OAI: oai:DiVA.org:kth-181591DiVA: diva2:900571
20th European Symposium on Research in Computer Security, ESORICS 2015; Vienna; Austria
FunderSwedish Foundation for Strategic Research
QC 201602042016-02-042016-02-022016-06-10Bibliographically approved