Abstrakt. I den här artikeln presenterar vi en programlogik för att bevisa att ett program inte släpper information om känsliga data på ett oavsiktligt sätt. Det viktigaste inslaget i logiken är att den ger en formell säkerhetsgaranti samtidigt som den stöder "avklassificeringspolicyer" som beskriver exakta förhållanden under vilka en del känsliga data kan släppas. Vi utnyttjar Hoare Logics makt för att uttrycka politiken och säkerhetsgarantin i form av statliga predikat. Detta gör att vårt system kan vara mycket mer specifikt när det gäller avklassificeringsvillkor än de flesta andra informationssystem. Logiken är utformad för att resonera om ett C-liknande, tvingande språk med pekarmanipulering och alias. Vi använder oss därför av idéer från Separation Logic till att resonera om data i högen.
Costanzo och Shao REF föreslår en sekventiell separationslogik för resonemang om informationsflödet.
A Separation Logic for Enforcing Declarative Information Flow Control Policies
{'venue': 'POST', 'journal': None, 'mag_field_of_study': ['Computer Science']}