About / Advertise
Ett formellt bevis för att OS-kärnan Pike OS är korrekt. Det håller operativsystemets ägare Sysgo på att ta fram.
Sysgo blir därmed bli nummer två med att formellt bevisa ett kommersiellt operativsystems korrekthet. Först ut var australiska Open Kernel Labs och dess kärna OKL4 Secure (länk).– Vi anser oss faktiskt ha bättre förutsättningar än de, säger Jacques Brygier, marknadschef på Sysgo.
– Redan när vi började konstruera Pike OS för flera år sedan tog en ordentlig titt på L4 och sedan bestämde oss för att göra en egen implementation. Vi ville adressera säkerhet och sekretessfrågor från grunder. Det var frågor som inte adresserades av L4.
Pike OS och OKL4 är båda mikrokärnor som båda bygger på L4, en forskningsidé från 1990-talet som idag når ut i kommersiella produkter.
Det som bevisas i sådana här sammanhang är att implementationen överensstämmer med en formell specifikation av operativsystemet.
Sysgos bevis beräknas vara komplett i år. Hittills har företaget bland annat verifierat några systemanrop, ett funktionsbibliotek för generell manipulering av listor och detaljer i interruptfunktionaliteten. Just nu bevisar man jobbar företaget vidare med minnesadressöversättning och minnesseparation.
I dagens läge ställs inga formella beviskrav inom de standarder som används för att certifiera en kärna för användning i exempelvis säkerhetskritiska system.
