Abstract-Vi tar upp problemet med programverifiering för informationsflödespolicyer genom symboliskt utförande och modellkontroll. Icke-inblandningsliknande säkerhetspolicy formaliseras med hjälp av epistemisk logik. Vi visar hur policyn kan verifieras med hjälp av en kombination av konkolisk testning och SMT-lösning. Som vi visar kan många scenarier som betraktas som knepiga i litteraturen lösas exakt med hjälp av det föreslagna tillvägagångssättet. Detta bekräftas av experiment utförda med ENCOVER, ett verktyg baserat på Java PathFinder och Z3, som vi har utvecklat för epistemisk icke-interferens konkolisk verifiering.
ENCoVer REF använder epistemisk logik och använder symbolisk körning (konkolisk testning) för att kontrollera icke-interferens för Java-program.
ENCoVer: Symbolic Exploration for Information Flow Security
{'venue': '2012 IEEE 25th Computer Security Foundations Symposium', 'journal': '2012 IEEE 25th Computer Security Foundations Symposium', 'mag_field_of_study': ['Computer Science']}