Provably Secure Execution Platforms for Embedded Systems
- Reference number
- RIT10-0069
- Start and end dates
- 110901-170831
- Amount granted
- 19 603 404 SEK
- Administrative organization
- KTH - Royal Institute of Technology
- Research area
- Information, Communication and Systems Technology
Summary
The PROSPER project will develop provably secure execution platforms for embedded systems together with a toolbox for formal modeling and verification. The platform runs a hypervisor core with strong isolation capabilities, on top of which dedicated security services such as cryptographic functions, application and resource monitoring, and information flow control manage the hosted applications. The toolbox comprises a verification platform, a refinement framework for incremental hypervisor and security service implementation, and a library of proof automation strategies. The project will produce a demonstrator consisting of a family of hypervisors for a chosen set of embedded architectures, the toolbox, the actual correctness proofs, and a concrete application in the form of a purely software based SIM as a secure service. The project plan envisages in its first stage (year 1-2) the development of a hypervisor for the ARM processor family for embedded architectures with a simple security service on top, a secure isolation model formalized in the verification platform, and correctness proofs of isolation. In the later stages (years 3-5) the MIPS processor family will be accommodated, the remaining security services will be added and formalized, and their security properties will be proved correct with the appropriate extensions of the toolbox. PROSPER will further result in 3 doctoral theses and a host of publications in recognized journals and conferences.
Popular science description
Inbyggda system finns överallt, såväl i samhället som i våra hem. De används till kommunikation, för att styra och kontrollera samt för att samla in information. Komplexiteten hos ett inbyggt system varierar från avancerade enheter, såsom en mobiltelefon, till mycket små system likt en trådlös sensor för temperaturmätning. Det en klar trend att allt fler inbyggda system blir uppkopplade samt att de i hög utsträckning är byggda på öppen programvara. Detta ger många fördelar, framförallt bidrar det till att man snabbt och kostnadseffektivt kan få fram nya produkter. Exponeringen mot internet medför dock ökade risker och hot mot funktionerna i systemen. Det blir allt svårare att ha full kontroll på den programvara som används, och nya kanaler att attackera mjukvaran i systemen kommer ständigt till. Vi har de senaste åren följdriktigt sett allt fler exempel på infekterade inbyggda system. Detta kan få mycket allvarliga konsekvenser. Ett aktuellt exempel är den så kallade Stuxnet-datamasken som attackerar kontrollsystem och har till och med spridit sig till enheter i kärnkraftverk. Vi kan alltså konstatera att det behövs nya kraftfulla återgärder för ökat skydd av inbyggda system. Forskningen på området ligger efter, och efterfrågan på nya lösningar som gör systemen säkra är mycket stor, både i svensk och utländsk industri. PROSPER-projektet arbetar med just detta, det vill säga med att ta fram ny programvara, för att skydda exekveringen och verifiera mjukvaran i inbyggda system. Projektet syftar till att med hjälp av så kallade virtualiseringstekniker införa ett kompakt och formellt verifierat mjukvarulager i olika inbyggda system. Detta lager används för att skydda tjänsterna som exekverar på de inbyggda systemen, genom att isolera säkerhetskritiska funktioner från icke säkerhetskritiska samt övervaka operativsystem och viktiga applikationer. Stor vikt i projektet läggs på att formellt verifiera säkerheten och korrektheten i virtualiseringsmjukvaran samt att kunna göra denna verifiering automatiskt med hjälp av mjukvaruverktyg, som projektet tar fram. PROSPER har ett tätt samarbete med Ericsson och ST-Ericsson, för att på så sätt säkerställa att arkitekturerna, för de inbyggda system vi arbetar med, är de som kommer ut på marknaden i framtiden. Arbetet ska frambringa minst tre nya doktorer, ett stort antal publikationer i välrenommerade vetenskapliga tidskrifter och konferenser samt öppen källkod som vinner erkännande och global spridning.