Abstract-Vi föreslår ett nytt system för att bevisa administrativ rollbaserad åtkomstkontroll (ARBAC) politik korrekt med avseende på säkerhetsegenskaper med hjälp av de kraftfulla abstraktionbaserade verktyg som finns för programverifiering. Vårt system använder en kombination av abstraktion och reduktion för att programverifiering för att utföra säkerhetsanalys. Vi konverterar ARBAC politik till tvingande program som simulerar politiken abstrakt, och sedan använda ytterligare abstrakt-tolkning tekniker från programanalys för att analysera programmen för att bevisa politiken säker. Vi hävdar att de aggressiva set-abstraktioner och numerisk-abstraktioner vi använder är naturliga och lämpliga i passerkontroll inställning. Vi implementerar vårt schema med hjälp av ett verktyg som kallas VAC som översätter ARBAC-policyer till tvingande program följt av en intervallbaserad statisk analys av programmet, och visar att vi effektivt kan bevisa åtkomstkontroll policyer korrekt. Det viktigaste inslaget i vårt tillvägagångssätt är de abstraktionssystem vi utvecklar och minskningen av rollbaserad åtkomstkontrollsäkerhet (som inte har något att göra med program) till programverifieringsproblem.
Ferrara et al REF konverterade ARBAC-policyer till tvingande program och tillämpade abstrakt-tolkning tekniker för att analysera de konverterade programmen.
Security Analysis of Role-based Access Control through Program Verification
{'venue': '2012 IEEE 25th Computer Security Foundations Symposium', 'journal': '2012 IEEE 25th Computer Security Foundations Symposium', 'mag_field_of_study': ['Computer Science']}