Till skillnad från säkerhetsegenskaper som kräver frånvaron av ett "dåligt" programspår, föreskriver k-säkerhetsegenskaper frånvaron av en "dålig" interaktion mellan k-spår. Exempel på k-säkerhetsegenskaper är transitivitet, associativitet, antisymmetri och monotonitet. Detta papper presenterar en ljud och relativt komplett analys, kallad Cartesian Hoare Logic (CHL), för att kontrollera k-säkerhetsegenskaper. Vår programlogik är utformad med automatisering och skalbarhet i åtanke, så att vi kan formulera en verifieringsalgoritm som automatiserar resonemang i CHL. Vi har implementerat vår verifieringsalgoritm i ett helautomatiskt verktyg kallat DESCARTES, som kan användas för att analysera alla k-säkerhetsegenskaper hos Javaprogram. Vi har använt DESCARTES för att analysera användardefinierade relationsoperatörer och visa att DESCARTES är effektivt för att verifiera (eller hitta brott mot) flera k-säkerhetsegenskaper.
Cartesian Hoare logik REF (CHL) utvidgar standard Hoare logik till att resonera om k-säkerhet egenskaper relationella spår (input / output par av ett program).
Cartesian hoare logic for verifying k-safety properties
{'venue': 'PLDI 2016', 'journal': None, 'mag_field_of_study': ['Computer Science']}