Vi betraktar problemet med att statiskt kontrollera att koden för ett system överensstämmer med en uttrycklig tillståndspolicy. I en distribuerad inställning, någon del av systemet kan äventyras, det vill säga vissa noder av systemet och deras säkerhetsbehörigheter kan vara under kontroll av en angripare. För att bidra till att förutse och begränsa effekterna av en sådan partiell kompromiss förespråkar vi en logikbaserad politik som uttryckligen registrerar beroenden mellan huvudmännen. Vi föreslår ett uppfyllandekriterium, säkerhet trots kompromissade uppdragsgivare, så att ett ogiltigt tillståndsbeslut vid en kompromisslös nod kan uppstå endast när noder som beslutet logiskt beror på äventyras. Vi formaliserar detta kriterium i en processkalkyl och presenterar en verifieringsteknik baserad på ett typsystem. Därför kan vi kontrollera policyöverensstämmelse av kod som använder ett brett spektrum av säkerhetsmekanismer som finns i distribuerade system, allt från säkra kanaler ner till kryptografiska primitiva, inklusive kryptering och publickey signaturer.
Fournet och al. REF föreslog ett typsystem som kan användas för att analysera överensstämmelse med behörighetsprinciper i närvaro av kompromissade deltagare.
A Type Discipline for Authorization in Distributed Systems
{'venue': "20th IEEE Computer Security Foundations Symposium (CSF'07)", 'journal': "20th IEEE Computer Security Foundations Symposium (CSF'07)", 'mag_field_of_study': ['Computer Science']}