Abstrakt. Separation mellan processer ovanpå ett operativsystem eller mellan gäster i en virtualiserad miljö är avgörande för att skapa säkerhet på moderna plattformar. Ett viktigt krav för den underliggande hårdvaran är förmågan att stödja flera partitioner som körs på den delade maskinvaran utan otillbörlig störning. För moderna processorarkitekturer - med hårdvarustöd för minneshantering, flera driftssätt och I/O-gränssnitt - är detta en känslig fråga som kräver djup analys på både instruktionsnivå och processorimplementeringsnivå. I ett första försök att noggrant besvara denna typ av frågor introducerade vi i tidigare arbete en informationsflödesanalys av användarprogram exekvering på en ARMv7-plattform med hårdvarustödd minnesskydd, men utan I/O. Analysen utfördes som ett semiautomatiskt korrektursökningsförfarande ovanpå en ARMv7 ISA-modell som implementerades i Cambridge HOL4 theorem prover av Fox et al. Den begränsade plattformens funktionalitet gör dock analysen av begränsat praktiskt värde. I detta dokument lägger vi till stöd för enheter, inklusive DMA, till analysen. I detta syfte föreslår vi ett tillvägagångssätt för modellering av enheter baserat på idén att utföra anordningar på ett icke-deterministiskt sätt parallellt med den (enkärnig) deterministiska processorn, som täcker en fin granularitet av interaktioner mellan modellkomponenterna. Baserat på denna modell och med ARMv7 ISA som exempel, tillhandahåller vi HOL4-bevis på flera icke-interferensorienterade isoleringsegenskaper för en partition som utförs i närvaro av enheter som potentiellt använder DMA eller avbryter.
Schwarz et al REF föreslog en enhetsmodell där alla enheter utförs icke-deterministiskt parallellt med en enda kärnprocessor.
Formal Verification of Secure User Mode Device Execution with DMA
{'venue': 'Haifa Verification Conference', 'journal': None, 'mag_field_of_study': ['Computer Science']}