Patrick Cousot - Principles of abstract interpretation

Principles of Abstract Interpretation

Patrick Cousot

The MIT Press
Cambridge, Massachusetts
London, England

2021 2021 Massachusetts Institute of Technology

All rights reserved. No part of this book may be reproduced in any form by any electronic or mechanical means (including photocopying, recording, or information storage and retrieval) without permission in writing from the publisher.

Library of Congress Cataloging-in-Publication Data

Names: Cousot, Patrick, 1948 author.

Title: Principles of abstract interpretation / Patrick Cousot.

Description: Cambridge, Massachusetts: The MIT Press, [2021] | Includes bibliographical

references and index.

Identifiers: LCCN 2020041256 | ISBN 9780262044905

Subjects: LCSH: Semantic computing. | Abstract data types (Computer science)

Classification: LCC QA76.5913.C578 2021 | DDC 006dc23

LC record available at https://lccn.loc.gov/2020041256

d_r0

To Radhia Cousot, my daughters Camille and Rebecca, my sons Laurent and Thibault, and my grandchildren Margot, Sacha, Maxime, and Mal.

List of Figures

Syntax tree of the labeled program (4.1)

Labels of a statement

Upper closure operator

Higher-order Galois connection

Galois connection , , , upper closure operator , and lower closure operator

Fixpoints of increasing and nonincreasing functions

Iteration

Continuity

Fixpoint abstraction

Transformer abstraction

Fixpoint overapproximation

Fixpoint abstraction

On commutation

Example of structural Hoare triple derivation

The congruence complete lattice

Interval complete lattice

Inductive and coinductive fixpoint iterations

Roy-Floyd-Warshall shortest distance algorithm

The Roy-Floyd-Warshall algorithm

Hierarchy of points-to static analyzers

The subsumption algorithm

The greatest lower bound algorithm

The least upper bound algorithm

Monomorphic typing rules

Monotype inference rules for expressions

Impossible failure

Possible success

After a short introduction to abstract interpretation (chapter 1), we provide a very minimal presentation of the core concepts of the theory and applications of abstract interpretation (chapter 3).

These core concepts of abstract interpretation can be presented as one or two classes of programming languages, compilation, program analysis, formal methods, or software engineering courses.

Before introducing abstract interpretation, we recall the basic concepts of set theory which are used almost everywhere in computer science and can be self-studied (chapter 2).

Contents

Since the beginning of computer science, in the 1940s, programmers have been writing programs that are increasingly powerful but still filled with errors. The most common method for tracking errors in programs is debugging. Run the program on as many data as possible and track for results that look incorrect. The obvious limitation is that only a finite number of casesindeed very fewcan be considered among all possible cases. Moreover, some properties cannot be checked in this wayfor example, that a program will never stop (unless interrupted).

Therefore, since the 1940s, great programmers have thought about writing programs without errors. Alan Turing [] and exemplified by programs of about 30 lines.

Things have changed a lot since then. Programs are much largermillions of lines are not uncommon. The program properties to be checked are much more complicated: for example, security and privacy properties that no one has yet been able to define precisely enough to anticipate all possible attacks and leaks. There are many more programmers, not all of them scientists as great as Alan Turing. Furthermore even computer hardware has bugs. Computer science applications are no longer created for a few scientists but are offered commercially to an extremely large public. Moreover, program bugs can and do kill people.

Still, debugging is going on. It is inexpensive, because it is performed mainly by end users who have no alternative to software that needs debugging. At root, programmers are not responsible for their errors. In addition, the no-warranty clause in software license agreements typically states that the licensor makes no guarantees regarding the utility, usability, accuracy, or performance of the software and related documentation or information. The software is provided as is, with faults, defects, errors and viruses and without warranty of any kind. The licensor does not warrant that the software will be free of bugs, errors, viruses, or other defects, and the licensor shall have no liability of any kind for the use of or inability to use the software, the software content, or any associated service.

This disgraceful Dantean situation is specific to computer science, in particular because of the lack of usable tools for engineers. Progress is needed. The final goal is to check programs for correctness without ever omitting a case that might go wrong. This is the ultimate, perhaps unfeasible, and surely not fully automatizable (see chapter 9) objective of formal methods.

Abstract interpretation [] for an informal introduction). It formalizes formal methods and allows discussing the guarantees they provide, such as soundness (the conclusions about programs are always correct under suitable explicitly stated hypotheses), completeness (all true facts are provable), or incompleteness (showing the limits of applicability of the formal method). For example, abstract interpretation explains the power and limits of debugging, deductive/proof/verification methods, model checking, static analysis, and so forth.

Abstract interpretation is applied mainly to design semantics, proof methods, and static analysis of programs. The semantics of a programming language formally defines all possible executions of its programs at various levels of abstraction. Proof methods can be used to prove (manually or using theorem provers) that the semantics of a program satisfies some specification, which is a property of executions defining what the program is supposed to do. Static analyzers are programs that automatically extract properties of programs semantics (i.e., properties of their executions) using only the program text, without running the programs on a computer.

The objective of this book is to introduce the theory of abstract interpretation and discuss its application to the semantics, specification, verification, and static program analysis of safety and security properties of programs. We focus on principles and breadth of applicability. We do not consider in great depth the algorithmic aspects (data structures and complexity); instead we refer to the literature for the improvement of the readers knowledge. The book is intended for readers interested in the theory of abstract interpretation, the understanding of formal methods, and the design of verifiers and static analyzers. For those interested only in the use of such static analyzers,