Abstract-Access-kontrollsystem används i stor utsträckning för att skydda datorsystem. De definieras i form av riktlinjer för tillträdeskontroll som reglerar tillgången till systemresurser. I detta dokument inför vi en formellt definierad, fullständigt genomförd ram för specificering, analys och tillämpning av attributbaserade riktlinjer för tillträdeskontroll. Ramen vilar på FACPL, ett språk med en kompakt, men ändå uttrycksfull, syntax för specificering av real-world access control policys och med en strikt definierad denotational semantik. Ramen möjliggör automatisk kontroll av egenskaper både när det gäller de tillstånd som krävs genom en enda policy och förhållandet mellan flera policys. Analysens effektivitet och prestanda bygger på en semantisk konservering av FACPL-politiken i form av SMT-formler och på användningen av effektiva SMT-lösare. I vår analys tar vi uttryckligen upp några viktiga aspekter av utvärderingen av politiken, såsom saknade attribut, felaktiga värden och skyldigheter, som i stället förbises i andra förslag. Ramverket stöds av Java-baserade verktyg, bland annat en Eclipse-baserad IDE som erbjuder en skräddarsydd utvecklings- och analysmiljö för FACPL-policyer och ett Java-bibliotek för policygenomförande. Vi illustrerar ramverket och dess formella beståndsdelar med hjälp av en fallstudie för e-hälsa, medan dess effektivitet bedöms med hjälp av resultatstresstester och experiment på ett väletablerat riktmärke.
Formal Access Control Policy Language (FACPL) är ett formellt definierat språk för specifikation, analys och tillämpning av attributbaserade åtkomstkontrollpolicyer, inspirerade av XACML REF.
A Rigorous Framework for Specification, Analysis and Enforcement of Access Control Policies
{'venue': 'IEEE Transactions on Software Engineering', 'journal': 'IEEE Transactions on Software Engineering', 'mag_field_of_study': ['Computer Science']}