Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky
Semantics-based program analysis uses an abstract semantics of programs/systems to statically determine run-time properties. Classic examples from compiler technology include analyses to support constant propagation and constant folding transformations and estimation of pointer values to prevent buffer overruns. More recent examples include the estimation of information flows (to enforce security constraints) and estimation of non-functional properties such as timing (to determine worst case execution times in hard real-time applications). The classical approaches are based on semantics involving discrete mathematics. Paralleling trends in model-checking, there have been recent moves towards using probabilistic and quantitative methods in program analysis. In this paper we start by reviewing both classical and probabilistic/quantitative approaches to program analysis. We shall provide a comparison of the two approaches. We shall use a simple information flow analysis to exemplify the classical approach. The existence of covert information flows through timing channels are difficult to detect using classical techniques; we show how such problems can be addressed using probabilistic techniques.
Source: COMPUTER JOURNAL Volume: 53 Issue: 6 Pages: 871-880 DOI: 10.1093/comjnl/bxp033 Published: JUL 2010 Accession Number: WOS:000279185400019 Document Type: Article Author Keywords: program analysis; semantics; abstract interpretation KeyWords Plus: INFORMATION-FLOW Reprint Address: Hankin, C (reprint author) Univ London Imperial Coll Sci Technol & Med, Dept Comp, 180 Queens Gate, London SW7 2AZ, England. Addresses: Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England Univ Verona, Dept Comp Sci, I-37134 Verona, Italy E-mail Addresses: firstname.lastname@example.org Publisher: OXFORD UNIV PRESS, GREAT CLARENDON ST, OXFORD OX2 6DP, ENGLAND Web of Science Categories: Computer Science, Hardware & Architecture; Computer Science, Information Systems; Computer Science, Software Engineering; Computer Science, Theory & Methods Research Areas: Computer Science IDS Number: 616CJ ISSN: 0010-4620 Full Text: http://comjnl.oxfordjournals.org/content/53/6/871