Vi visar genom ett antal exempel att säkerhetsegenskaper i informationsflödet kan bevisas genom abstrakta arkitektoniska beskrivningar, som endast beskriver ett systems kausalstruktur och lokala egenskaper hos betrodda komponenter. Vi specificerar dessa arkitektoniska beskrivningar av system genom att generalisera intransitiva icke-interferens policyer för att erkänna möjligheten att filtrera information som skickas mellan kommunicerande domäner. Ett begrepp om förfining av sådana systemarkitekturer utvecklas som stöder uppifrån-och-ned utveckling av arkitektoniska specifikationer och bevis genom abstraktion av informationssäkerhet egenskaper. Vi visar också att i en konkret miljö där kausalstrukturen upprätthålls genom tillträdeskontroll är en statisk kontroll av inställning av tillträdeskontroll plus lokal kontroll av de betrodda komponenterna tillräcklig för att bevisa att en generaliserad intransitiv icke-interferenspolicy är tillfredsställd. Ytterligare nyckelord och fraser: Informationsflödessäkerhet, epistemisk logik, systemarkitektur, intransitiv icke-interferens Stephen Chong och Ron van der Meyden. Denna förordning träder i kraft den tjugonde dagen efter det att den har offentliggjorts i Europeiska unionens officiella tidning. Använda arkitektur för att resonera om informationssäkerhet. m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m m. [2008] omfattar den en konstruktionsprocess på två nivåer, bestående av en policynivå och en resursdelningsnivå. På policynivå beskrivs systemet av en arkitektur i form av en graf, där hörnen motsvarar komponenter och kanterna anger tillåten kommunikation mellan komponenter. I detta avseende är arkitekturen som en intransitiv icke-inblandningssäkerhetspolitik [Haigh and Young 1987; Rushby 1992; van der Meyden 2007]. På politisk nivå kan man också specificera vilka komponenter som är betrodda och vilka lokala politiska åtgärder som dessa komponenter är betrodda att genomföra. Enligt MILS vision, att bygga ett system enligt arkitekturen, genom att komponera komponenter som uppfyller deras lokala politik, bör resultera i systemet som uppfyller globala säkerhets- och säkerhetsegenskaper. På resursdelningsnivå planerar MILS att använda en rad infrastrukturella mekanismer för att se till att politiken för arkitektoniskt informationsflöde efterlevs trots att komponenter delar resurser som processorer, filsystem och nätverkslänkar. Dessa mekanismer kan omfatta fysisk isolering, separationskärnor, periodbehandling, kryptografi och åtskiljande nätverksinfrastruktur. Avsikten är att denna infrastruktur ska utvecklas till en hög säkerhetsnivå så att ett systemsäkringsfall kan erhållas genom sammansättningen av försäkringsfallen för betrodda komponenter och systeminfrastrukturer. Förhoppningen är att detta kommer att möjliggöra en COTS-liknande marknad för infrastrukturmekanismer och betrodda komponenter. Det viktigaste bidraget i denna artikel är att visa, genom flera exempel, att det i själva verket är möjligt, enligt vad som förutses i MILS litteratur, att härleda intressant information säkerhet egenskaper kompositionellt från en hög nivå specifikation av betrodda komponenter och deras arkitektoniska struktur. Vi fokuserar på kompositionstänkande kring säkerhetsfastigheter i informationsflödet. Vi presenterar en ram som gör det möjligt att specificera en systemarkitektur med lokala begränsningar för vissa systemkomponenter. För att ge den arkitektoniska strukturen en exakt innebörd utvidgar vi semantiken för en intransitiv icke-interferenspolitik som utvecklats av van der Meyden [2007]. Dessa riktlinjer är i form av en graf, där hörnen motsvarar systemkomponenter, och en kant från komponent u till komponent v anger att information är tillåten att strömma från u direkt till v. Denna semantik uttrycks i en asynkron modell av beräkning och fångar en uppfattning om information tillgänglig för en angripare som inte har tillgång till timing information. En arkitektonisk tolkning av denna semantik har tidigare gjorts [van der Meyden 2012]. För att uttrycka begränsningar på betrodda komponenter utökar vi arkitekturer genom att märka kanter mellan komponenter med funktioner som ytterligare begränsar den information som tillåts flöda längs kanterna. Ett av verkets bidrag är att ge en formell semantik till de berikade arkitekturer som inkluderar dessa nya typer av kanter. Vi utvecklar också en teori om förfining för dessa berikade arkitekturer, vilket möjliggör uppifrån-och-ned, korrekt-bevarande utveckling av arkitektoniska specifikationer. Det möjliggör också enkla bevis på informationssäkerhet egenskaper på komplexa arkitekturer som kan erhållas med hjälp av en abstraktion av denna arkitektur. Vi demonstrerar användningen av ramverket genom exempel som motiveras av system med intressanta säkerhetskrav. Dessa inkluderar flera nivåer säkra databaser, Starlight Interactive Link [Anderson et al. 1996 ], en pålitlig nedgraderare, och ett enkelt elektroniskt valsystem. I varje exempel finns det en tillämpningsspecifik informationsflöde säkerhetsfastighet, uttryckt i en logik av kunskap, som ska genomdrivas. För att upprätthålla dessa egenskaper identifierar vi i varje exempel en arkitektonisk struktur och en matematiskt exakt uppsättning lokala begränsningar för de betrodda komponenterna. Vi visar för varje exempel att dess specifika säkerhetsfastighet uppstår som en följd av samspelet mellan lokala begränsningar och den arkitektoniska strukturen. I varje exempel, våra resultat visar att för alla system som överensstämmer med arkitekturen, om
Chong och van der Meyden REF diskuterar informationsflödespolicyer (så kallade arkitekturer), där filterfunktioner används för att begränsa vilken information som kan flöda mellan domäner, tillsammans med en tolkning av de resulterande säkerhetsegenskaperna i termer av en epistemisk logik.
Using Architecture to Reason about Information Security
{'venue': 'TSEC', 'journal': None, 'mag_field_of_study': ['Computer Science']}