About / Advertise
EMBEDDED WORLD Franska Prove & run har matematiskt bevisat att det inte finns några buggar i säkerhetsfunktionerna i företagets realtidsoperativsystem Provencore.
Säkerhetsfunktionerna i fråga är bland annat minnesisolering av olika program på processorn.
Fler företag ger samma skydd, i så kallade hypervisorer, men Prove & run har matematiskt bevisat att deras minnesmodell fungerar och att deras kod implementerar modellen korrekt.
Att det finns ett bevis skyddar mot så kallade nolldagssårbarheter som beror av att någon hittat och utnyttjar en bugg i ditt operativsystem. Det kan inte finnas några buggar i Provencore enligt det matematiska beviset.
Den senaste versionen heter Provencore-M och stöder ARM Cortex M23 och M33-cpu:er. De använder arkitekturen ARMv8-M och har ett hårdvarustöd för säkerhet kallat Trustzone.
ARMv8-M-processorer finns inte än, men kommer snart. I bilden ovan ser du ARMv8-M-processor emuleras i en FPGA, snurrandes på Provencore-M.
Operativsystemet vann mässans Embedded award i kategorin programvara.
Provencore stöder sedan tidigare ARM-kärnor med Trustzone och ARM-kärnor med hypervisorstöd, som Cortex A-familjen. Operativsystemet kan köra på samma processor som rika operativsystem som Linux, helt informationsisolerad från dessa.
Prestanda beskrivs av företaget som varande i nivå med dagens realtidsoperativsystem.
Prove & run saluför dessutom sin egen hypervisor, också den bevisad.
All kod har utvecklats helt och hållet på företaget, vilket är en följd av hur produkterna konstruerats. De har byggts från grunden och av C-kod generad från verktyg och modeller som i sin tur varit bevisade.
Ett exempel på användning är smarta elmätare eller andra tillämpningar som räknar pengar. Räknandet måste ske bakom ett ogenomträngligt skydd, minnesisolering, för att inte kunna manipuleras. Och det får inte finnas okända programmeringsfel som någon kan råka upptäcka och utnyttja – därför det matematiska beviset.
Andra tillämpningar finns inom industri, fordon och generellt inom uppkopplade inbyggda system.
Tillämpningar utvecklas i Prove & runs egen utvecklingsmiljö.
Företaget har funnits i sex år. Upphovsmannen till tekniken är företagets grundare Dominique Bolignano.
Elektroniktidningen har tidigare skrivit om ett annat korrekthetsbevisat operativsystem, SEL4, som numera finns att tanka hem här i form av öppen källkod.
NSA-avhopparen Edward Snowden rekommenderar ett öppenkods-OS kallat Cubes OS som inte är korrekthetsbevisat, men adresserar samma tillämpningsområde som Prove & run, att informationsisolera program på samma processor från varandra.
