Uttagsskyddsmodell
Anslagsskyddsmodellen är en formell modell som används inom datasäkerhetsområdet för att fastställa eller motbevisa säkerheten för ett givet datorsystem som följer specifika regler. Den visar att även om frågan om säkerhet i allmänhet är oavgörbar , är den för specifika system avgörbar i linjär tid.
Modellen representerar ett system som riktad graf , där hörn är antingen subjekt eller objekt. Kanterna mellan dem är märkta och etiketten indikerar de rättigheter som kantens källa har över destinationen. Två rättigheter förekommer i varje instans av modellen: ta och bevilja . De spelar en speciell roll i reglerna för omskrivning av grafer som beskriver tillåtna ändringar av grafen.
Det finns totalt fyra sådana regler:
- take-regeln tillåter ett subjekt att ta rättigheter till ett annat objekt (lägg till en kant som kommer från subjektet)
- bevilja regeln tillåter en subjekt att ge egna rättigheter till ett annat objekt (lägg till en kant som slutar vid subjektet)
- skapa regel tillåter ett subjekt att skapa nya objekt (lägg till en vertex och en kant från subjektet till den nya vertexen)
- ta bort regel tillåter ett ämne att ta bort rättigheter som det har över på ett annat objekt (ta bort en kant som har sitt ursprung i ämnet)
Förutsättningar för :
- ämne s har rätt Ta för o .
- objekt o har rätt r på sid .
Förutsättningar för :
- ämne s har rätt Bidrag för o .
- s har rätt r på sid .
Med hjälp av reglerna för skyddsmodellen för beviljande av bidrag kan man reproducera i vilka stater ett system kan förändras, med avseende på fördelningen av rättigheter. Därför kan man visa om rättigheter kan läcka med avseende på en given säkerhetsmodell.
- Lipton, Richard J .; Snyder, Lawrence (1977). "En linjär tidsalgoritm för att bestämma ämnessäkerhet" ( PDF ) . Journal of the ACM . 24 (3): 455–464. CiteSeerX 10.1.1.149.4807 . doi : 10.1145/322017.322025 .
- Bishop, Matt (2004). Datorsäkerhet: konst och vetenskap . Addison-Wesley.