Alessandra Di Pierro, Chris Hankin and Herbert Wiklicky

Abstract:

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: clh@doc.ic.ac.uk
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

Categories: Publications