Google har præsenteret det software- og hardwarekompleks, Open Se Cura, designet til at forenkle oprettelsen af sikre chips til maskinlæring og kunstig intelligens. Projektet omfatter operativsystemet CantripOS og hardware baseret på OpenTitan-platformen samt en processorarkitektur bygget på RISC-V. Under udviklingen blev Open Se Cura og CantripOS omtalt som Sparrow og KataOS, men for at undgå overlapning med andre projekter er de endelige produkter blevet omdøbt. Projektets resultater, herunder kildekoder til systemtjenester og RTL-schemas (Register Transfer Level), distribueres under Apache 2.0-licensen.
Operativsystemet CantripOS er baseret på mikro-kernen seL4, over hvilken et systemmiljø er implementeret i Rust. Der er givet et matematisk bevis for pålideligheden af mikro-kernen seL4, som viser, at koden fuldt ud overholder de specifikationer, der er angivet i det formelle sprog. Arkitekturen seL4 er bemærkelsesværdig ved at flytte dele af ressourcehåndteringen fra kernen til brugerområdet og anvende de samme adgangsgrænser til disse ressourcer som til brugerressourcer.
Mikro-kernen giver ikke færdige, høj-niveau abstraktioner til håndtering af filer, processer, netværksforbindelser osv., men den tilbyder kun minimale mekanismer til at styre adgangen til det fysiske adresseområde, afbrydelser og processorressourcer. Høj-niveau abstraktioner og drivere til interaktion med hardware implementeres separat oven på mikro-kernen i form af opgaver, der kører på brugerniveau. Adgangen for disse opgaver til mikro-kernens ressourcer organiseres ved hjælp af regler.
Alle komponenter i operativsystemet, bortset fra mikro-kernen, er oprindeligt skrevet i Rust ved hjælp af sikre programmeringsmetoder, der minimerer fejl ved håndtering af hukommelse. I Rust er blandt andet applikationsloaderen til seL4-miljøet, systemtjenesterne, rammerne til applikationsudvikling, API'et til adgang til systemopkald, procesmanageren og mekanismen til dynamisk hukommelsesfordeling skrevet.
Til den verificerede sammensætning benyttes værktøjet CAmkES, der udvikles af seL4-projektet. Til udvikling af slutapplikationer, som kan indlæses dynamisk af systemtjenester, anbefales det at anvende SDK AmbiML, mens IREE (Intermediate Representation Execution Environment) foreslås til udførelse af maskinlæringsmodeller. Komponenter skrevet i Rust og systemtjenester er udviklet ved hjælp af Cantrip-rammeværket.
Blandt anvendelsesområderne for platformen nævnes specialiserede chips, der kræver et særligt beskyttelsesniveau og bekræftelse af fravær af fejl. For eksempel kan platformen anvendes i maskinlæringsprodukter, der er relateret til behandling af fortrolige oplysninger, som f.eks. ansigtsgenkendelsessystemer og behandling af taler. Kombinationen af et logisk verificeret operativsystemkerne med betroede hardwarekomponenter (RoT, Root of Trust) sikrer, at hvis der opstår en fejl et sted i systemet, vil denne fejl ikke sprede sig til resten af systemet, især ikke til kernen og kritiske dele.
Foruden Google har den non-profit organisation lowRISC, som overvåger udviklingen af en fri mikroprocessor baseret på RISC-V-arkitekturen, samt virksomhederne Antmicro og VeriSilicon deltaget i udviklingen af værktøjer og infrastruktur. Den processor, der udvikles af lowRISC, blev brugt som kerne til opbygning af betroede hardwarekomponenter (RoT, Root of Trust). Antmicro leverede simulatoren Renode til projektet, som muliggør test af CantripOS og mikrokerne seL4 uden reel hardware. VeriSilicon delte sin erfaring inden for chipdesign og udvikling af BSP (Board Support Package).
Kilde: opennet.ru
