CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Testing noninterference, quickly

C. Hritcu ; John Hughes (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; A. Spector-Zabusky ; D. Vytiniotis ; A.A.D. Amorim ; L. Lampropoulos
ACM SIGPLAN Notices (1523-2867). Vol. 48 (2013), 9, p. 455-468.
[Artikel, refereegranskad vetenskaplig]

Information-flow control mechanisms are difficult to design and labor intensive to prove correct. To reduce the time wasted on proof attempts doomed to fail due to broken definitions, we advocate modern random testing techniques for finding counterexamples during the design process. We show how to use QuickCheck, a property-based random-testing tool, to guide the design of a simple information-flow abstract machine. We find that both sophisticated strategies for generating well-distributed random programs and readily falsifiable formulations of noninterference properties are critically important. We propose several approaches and evaluate their effectiveness on a collection of injected bugs of varying subtlety. We also present an effective technique for shrinking large counterexamples to minimal, easily comprehensible ones. Taken together, our best methods enable us to quickly and automatically generate simple counterexamples for all these bugs.



Denna post skapades 2016-04-21. Senast ändrad 2016-05-24.
CPL Pubid: 234998

 

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Programvaruteknik

Chalmers infrastruktur