\documentclass[12pt]{beamer}
\usetheme{Boadilla}

\title{Abstract interpretation}
\author{David Monniaux}
\institute{CNRS / VERIMAG}

\graphicspath{{../logos/}{../pics/}{pics/}}
\logo{\includegraphics[height=7mm]{logo_VERIMAG_vectorise}
\includegraphics[height=7mm]{WEB_CNRS-filaire-Quadri}}

\usepackage{tikz}
\usetikzlibrary{arrows,automata}

\usepackage{listings}
\lstset{language=C++,basicstyle={\rm\fontfamily{ppl}\selectfont},mathescape=true}

\AtBeginSection[]{\begin{frame}<beamer>
\tableofcontents[currentsection]
\end{frame}}

\AtBeginSubsection[]
{
    \begin{frame}{Outline}
        \tableofcontents[currentsection,currentsubsection]
    \end{frame}
}

\newcommand{\stress}[1]{\textbf{\textcolor{red}{#1}}}

% \newcommand{\finger}{\ding{43}~}
\newcommand{\finger}{$\Rightarrow$}

\usepackage{amssymb,amsfonts}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\abstr}[1]{#1^\sharp}

\begin{document}
\begin{frame}
\thispagestyle{empty}
\maketitle
\end{frame}

\begin{frame}{Grenoble}
\begin{center}
\includegraphics[height=6cm]{Grenoble_from_Moucherotte_IMG_0861_tuned_shrunk}
\end{center}
\end{frame}

\begin{frame}{VERIMAG}
\begin{center}
\includegraphics[height=5cm]{VERIMAG_P1160419_constrast_shrunk}
\end{center}

Joint lab between CNRS and Grenoble University

9 CNRS permanent researchers + 4 research engineers

23 professors
\end{frame}
% DR
% Halbwachs
% Maler
% Sifakis
% Graf
% CR1
% Monniaux
% Raymond
% Dang
% Iosif
% CR2
% Jobstmann

\section{Introduction}

\subsection{Position within other techniques}
\begin{frame}{Static analysis}

Establish automatically that a \stress{program} meets a \stress{specification}.
\bigskip

Specification can be:
\begin{enumerate}
\item Explicit, e.g. ``the program sorts the integer array given as input''.
\smallskip

Can be expressed by e.g. temporal logics, assertions\dots
\medskip

\item Implicit, e.g. ``the program never crashes due to division by zero, array overflow, bad pointer dereference''.
\smallskip

Easier for the programmer (no need to write anything in addition to the code).
\end{enumerate}
\end{frame}

\begin{frame}{Impossibilities}

Turing's Halting Problem / Rice's Theorem
\bigskip

Program analysis is impossible unless one condition is met:
\begin{enumerate}
\item Not fully automatic, requires user interaction.
\item Constrained enough class of programs.
\item Finite memory.
\item Finite number of program steps.
\item Analysis can answer \stress{false positives}.
\item Analysis can answer \stress{false negatives}.
\end{enumerate}
\end{frame}

\begin{frame}{User interaction}

Example: \stress{interactive theorem proving}.
\bigskip

Program analysis problems generally map to logics (e.g. Peano arithmetic)
with no decision procedure.
\medskip

(Actually a way to prove undecidability of such logics...)
\end{frame}

\begin{frame}{Finite memory}

Can enumerate \stress{reachable states} explicitly.
\bigskip

\stress{Computable} but costly: $n$ bits of memory in analyzed system

\finger $2^n$ states in analyzer
\end{frame}

\begin{frame}{Finite number of program steps}

Finite number of program steps

+ program statements with semantics in logics
e.g. linear arithmetic

\finger

\stress{Bounded model checking}.
\end{frame}

\begin{frame}{Analysis can produce false negatives}

\stress{False negative} = some bugs may be ignored
\bigskip

Examples of techniques:
\begin{itemize}
\item \stress{testing}
\item \href{http://www.coverity.com/}{Coverity}
\end{itemize}
\end{frame}

\begin{frame}{(Semantically sound) static analysis}

Deducing \stress{properties} of software
\begin{itemize}
\item From a mathematical model of its behaviour (\stress{semantics}).
\item Examples: ``no division by zero'', ``no assertion failure''
\item valid for \stress{all executions}
\item using safe \stress{over-approximation} of behaviors
\begin{itemize}
\item \stress{no false negatives}
\item maybe false positives (\stress{false alarms})
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{A central problem}

{\Large \stress{Higher precision (fewer false alarms)\\
vs scaling-up (low higher time/space costs)}}
\bigskip

Want to have them both?
\end{frame}

\subsection{A short chronology}

\begin{frame}{Ariane V, maiden flight, 1996}

\begin{center}
\includegraphics[height=7cm]{Ariane_60}
\end{center}
\end{frame}

\begin{frame}{Ariane V self-destructing}
\begin{center}
\includegraphics[height=7cm]{Ariane_138}
\end{center}
\end{frame}

\begin{frame}[fragile]
\frametitle{Arithmetic overflow}

\begin{minipage}{3cm}
\includegraphics[width=4cm]{Ariane_138}
\end{minipage}
\hfill
\begin{minipage}{7cm}
\begin{lstlisting}
x = computation_for_Ariane4();
y = (short int) x;
\end{lstlisting}

{\footnotesize (ok it was Ada, not C)}
\bigskip

\pause
\textcolor{violet}{\finger PolySpace Verifier (1996--)}\\(Deutsch et al.; commercial tool)
\bigskip

Bug found by \stress{direct automated analysis of the source code}.
\end{minipage}
\end{frame}

\begin{frame}{A modern airplane: Airbus A380}

\includegraphics[width=5.7cm]{Airbus_A380_P1230288_shrunk}
\hfill
\includegraphics[width=5.7cm]{Airbus_A380_cockpit_joystick}
\bigskip

\pause
\textcolor{violet}{\finger Astr\'ee (2002--)} (Cousot et al.)
\bigskip

Prove \stress{absence of bugs}.
\bigskip

I was a key member of Astr\'ee (now sold commercially).
\end{frame}

\begin{frame}{Safety-critical embedded systems}

\begin{itemize}
\item Airplanes (DO-178C), trains, space launchers
\item Nuclear plants, electrical grid controls
\item Medical devices
\end{itemize}
\bigskip

US Food and Drug Administration, action on \stress{infusion pumps} (2010).
\begin{center}
\includegraphics[height=4cm]{infusion_pump}
\end{center}
\end{frame}

\begin{frame}{At Microsoft...}

Microsoft Device Driver Verifier (from project SLAM)
\medskip

CodeContracts
\medskip

etc.
\end{frame}

\subsection{Basic ideas}

\begin{frame}{Large state spaces}

We cannot represent the \stress{concrete state space}~$X$.

Four 32-bit variables: $2^{128}$ states.

Too large for explicit-state model-checking (need to memorize all states in memory)...

and also for implicit-state model-checking (using clever structures e.g. BDDs)
\end{frame}

\begin{frame}{Solution}

Instead of a set of states $s \subseteq X$ use another $\abstr{s}$ simpler to represent.
\bigskip

e.g. with $X = \ZZ^2$, $s \subseteq X$ a set of pairs of integers,
$\abstr{s}$ a product of 2 intervals
\bigskip

\stress{We do not forget behaviors}: since $s \subseteq \abstr{s}$, cannot
forget any reachable state.
\end{frame}

% TODO drawing on various abstractions

% TODO basic concrete iteration scheme

\section{Boolean abstraction}

\subsection{Definition}
\begin{frame}{A system with infinite state}

State = a single integer variable~$x$
\bigskip

Initial state~: $x = 0$

Transition: $x' = x+1$
\bigskip

Reachable states: $\NN$.
\bigskip

Prove that $x \geq 0$ is an invariant.
\bigskip

\stress{Cannot compute} reachable states by iterations: infinite state space!
\end{frame}


\begin{frame}{A finite state system}

State = a single integer variable~$x$
\bigskip

Initial state: $x = 0$

Transition: $x' = x+1 \land x < 10^{10}$
\bigskip

Reachable states: $0 \leq x \leq 10^{10}$
\bigskip

\stress{No hope} by explicit model-checking techniques (computing the $10^{10}$ reachable states).
\end{frame}

\begin{frame}{Abstraction}

Introduce 5 ``abstract states''
\begin{itemize}
\item $A$: $x < 0$
\item $B$: $x = 0$
\item $C$: $0 < x < 10^{10}$
\item $D$: $x = 10^{10}$
\item $E$: $x > 10^{10}$
\end{itemize}

Put an arrow between abstract states $P$ and $Q$ iff one can move
from $p \in P$ to $q \in Q$.
\bigskip

Example: can move from $A$ to $B$ because $\{ x = -1 \} \in A$, can move to $\{ x' = 0 \} \in B$.
\end{frame}

\begin{frame}{Resulting system}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
                    semithick]
%\tikzstyle{every state}=[fill=red,draw=none,text=white]

  \node[state] (A)              {$A$};
  \node[initial,state] (B) [below of=A] {$B$};
  \node[state]         (C) [right of=B] {$C$};
  \node[state]         (D) [right of=C] {$D$};
  \node[state]         (E) [right of=D] {$E$};
  \path (A) edge node {} (B)
        (B) edge node {} (C)
        (C) edge [loop above] node {} (C)
            edge node {} (D);
\end{tikzpicture}

\begin{itemize}
\item $A$: $x < 0$
\item $B$: $x = 0$
\item $C$: $0 < x < 10^{10}$
\item $D$: $x = 10^{10}$
\item $E$: $x > 10^{10}$
\end{itemize}

\stress{No concrete transition is forgotten} and thus $E$ is \stress{unreachable}.
\end{frame}

\begin{frame}{Other example}
Initial state: $x = 0$
Transition: $x' = x+2 \land x \neq 10^{10}$
\bigskip

Reachable states: $0 \leq x < 10^{10} \land x \bmod 2 = 0$.
\end{frame}

\begin{frame}{Abstract graph}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
                    semithick]
%\tikzstyle{every state}=[fill=red,draw=none,text=white]

  \node[state] (A)              {$A$};
  \node[initial, state] (B) [below of=A] {$B$};
  \node[state]         (C) [right of=B] {$C$};
  \node[state]         (D) [right of=C] {$D$};
  \node[state]         (E) [right of=D] {$E$};
  \path (A) edge node {} (B)
        (B) edge node {} (C)
        (C) edge [loop above] node {} (C)
            edge node {} (D)
            edge [bend left] node {} (E);
\end{tikzpicture}

\begin{itemize}
\item $A$: $x < 0$
\item $B$: $x = 0$
\item $C$: $0 < x < 10^{10}$
\item $D$: $x = 10^{10}$
\item $E$: $x > 10^{10}$
\end{itemize}

$C \rightarrow E$ since $(10^{10}-1) \rightarrow (10^{10}+1)$.
\end{frame}

% \begin{frame}[fragile]
% \frametitle{Other loop}

% \lstset{language=C++}
% \begin{lstlisting}
% bool b = false;
% int x = 0;
% while (x < 12) {
%   x = x+1;
%   b = x >= 10;
% }
% \end{lstlisting}

% We hope to prove $b = \true$ at the end. Invariant:

% $(\neg b \land 0 \leq x < 10) \lor (b \land 10 \leq x < 12)$.
% \end{frame}

\begin{frame}{Over-approximation}

More behaviors:
\begin{itemize}
\item $E$ is concretely reachable.
\item $E$ is abstractly reachable
\end{itemize}
\bigskip

The analysis fails to prove the true property ``$E$ unreachable''.

\stress{Incomplete} method.
\bigskip

Remark: works with a better abstraction ($x < 10^{10}-1$).
\end{frame}


\begin{frame}{Principles of predicate abstraction}

\begin{itemize}
\item A finite set of \stress{predicates} (e.g. arithmetic constraints).
\item Construct a \stress{finite} system of abstract transitions between abstract states.
\item Each abstract state labeled by predicates, e.g. ex. $x < 0$.
\item Put an abstract transition from $A$ to $B$ iff one can move from a state $a \in A$ to a state $b \in B$.
\item \stress{Correctness} if an abstract state is unreachable, then so are the corresponding concrete states
\end{itemize}
\end{frame}

\begin{frame}{How to construct the abstract system}
Abstract states $A: x < 0$ and $C : 0 < x < 10^{10}$, transition relation $x' = x+1 \land x < 10^{10}$, can we move from $A$ to $C$?
\medskip

Otherwise said: is there a solution to $x < 0 \land (x'= x+1 \land x < 10^{10}) \land x' > 0$?
\medskip

Use \stress{satisfiability modulo theory} (SMT-solving).
\end{frame}

\begin{frame}{Computing the graph}

\begin{itemize}
\item Abstract states are couples (program point, set of predicates)
\item Apply SMT-solving to insert or not insert arrows.
\item Check if \stress{bad states} are unreachable.
\item If they are, \stress{win!}
\end{itemize}
\bigskip

...and if they are reachable?
\begin{itemize}
\item Maybe the abstraction is badly chosen?
\item Maybe the property to prove (unreachability of bad states) is false?
\end{itemize}
\end{frame}

\subsection{Some more examples}
\begin{frame}[fragile]
\frametitle{Exemple}
\begin{lstlisting}[numbers=left]
x = 0;
while (x < 10) {
  x = x+1;
}
y = 0;
while (y < x) {
  y = y+1;
}
\end{lstlisting}

Try predicates $x < 0$, $x = 0$, $x > 0$, $x < 10$, $x = 10$, $x > 10$, $y < 0$, $y = 0$, $y > 0$, $y < x$, $y = x$, $y > x$.
\medskip

Note: 12 predicates, so in the worst case $2^{12} = 4096$ combinations, some of which impossible (cannot have both $x < 0$ and $x > 0$ at same time).
\end{frame}

\begin{frame}[fragile]
\frametitle{Abstract automaton}

\begin{minipage}{5.7cm}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.4cm,
                    semithick]

  \node[initial,state] (A)      {$L_1$};
  \node[state] (B) [right of=A] {$L_2$};
  \node[state] (B2)[right of=B] {$L_2'$};
  \node[state] (C) [below of=B2] {$L_5$};
  \node[state] (D) [left of=C] {$L_6$};
  \node[state] (D2) [left of=D] {$L_6'$};
  \node[state] (E) [left of=D2] {$L_9$};
  \path (A) edge node {} (B)
        (B) edge [loop above] node {} (B)
        (B) edge node {} (B2)
        (B2) edge node {} (C)
        (C) edge node {} (D)
        (D) edge [loop below] node {} (D)
        (D) edge node {} (D2)
        (D2) edge node {} (E);
\end{tikzpicture}
\end{minipage}
\begin{minipage}{4.5cm}
\begin{lstlisting}[numbers=left]
x = 0;
while (x<10)
  x = x+1;
}
y = 0;
while (y<x) {
  y = y+1;
}
\end{lstlisting}
\end{minipage}

$L_1$: line~1, $x=0$\\
$L_2$: line~2, $0 < x<10$\\
$L_2'$: line~2: $x=10$\\
$L_5$: line~5: $x=10$\\
$L_6$: line~6: $x=10 \land y<x$\\
$L_6'$: line~6: $x=10 \land y=x$\\
$L_9$: line~9: $x=10 \land y=x$
\end{frame}

\begin{frame}[fragile]
\frametitle{Attention}
\begin{lstlisting}[numbers=left]
x = 0;
while (x != 10) {
  x = x+2;
}
\end{lstlisting}
Syntactic choice of predicates ($x < 0$, $x = 0$, $x > 0$, $x < 10$, $x = 10$, $x > 10$).
\end{frame}

\begin{frame}{Some solution?}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.5cm,
                    semithick]
\node[initial,state] (A) {\begin{tabular}{c}L1\\x=0\end{tabular}};
\node[state] (B) [right of=A] {\begin{tabular}{c}L2\\x=0\end{tabular}};
\node[state] (B2) [right of=B] {\begin{tabular}{c}L2\\0<x<10\end{tabular}};
\node[state] (B3) [below of=B2] {\begin{tabular}{c}L2\\x=10\end{tabular}};
\node[state] (C) [left of=B3] {\begin{tabular}{c}L5\\x=10\end{tabular}};

 \path (A)  edge node {} (B)
       (B)  edge node {} (B2)
            edge [loop above] node {} (B)
       (B2) edge node {} (B3)
       (B3) edge node {} (C);
\end{tikzpicture}
\end{frame}

\begin{frame}{Why is this solution wrong?}

This solution is \stress{sound} since it collects all behaviors of the program.
\bigskip

But you realize this only because you already know (in your head)
the set of reachable states! (This is cheating.)

\bigskip

This solution is not \stress{inductive}: it is possible to move from a state
represented in the graph to one that isn't!
\end{frame}

\begin{frame}[fragile]
\frametitle{Attention}
\begin{lstlisting}[numbers=left]
x = 0;
while (x != 10) {
  x = x+2;
}
\end{lstlisting}

At line~2, abstraction says $0 < x < 10$, thus $x = 9$ for instance.
\bigskip

$x=9$ is inaccessible \emph{in the concrete systems}! You know it only because you computed the set of reachable states $\{0, 2, 4, 6, 8\}$.
\bigskip

Need a transition from $0 < x < 10$ ($x = 9$)
to a new state $x > 10$ ($x = 11$).
\end{frame}

\begin{frame}{Human intuition vs automated computation}

The human sees the simple program and computes the set of reachable states $\{0, 2, 4, 6, 8\}$ knowing $x$ should be even.
\medskip

Then projects onto predicates, and $x > 10$ unreachable.
\bigskip

Automated computation does not see that $x$ is even because it was not given the predicate $x \bmod 2 = 0$.
\end{frame}

\begin{frame}{Not convinced?}

Let $P$ be a program where Boolean $x$ is not mentioned. Consider:
$x := 0$;
$P$;
$x := 1$
\bigskip

Use predicates $x=0$ et $x=1$. Give a finite automaton for the behaviors of the program wrt~$x$...
\bigskip

Automaton with two states $x=0$, $x=1$. Simple, hey?
\end{frame}

\begin{frame}{A minimal automaton (not inductive)}

If \stress{$P$ terminates}:

\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.5cm,
                    semithick]
\node[initial,state] (A) {$x=0$};
\node[state] (B) [right of=A] {$x=1$};
\path (A)  edge [loop above] node {} (A);
\path (A)  edge node {} (B);
\end{tikzpicture}
\bigskip

If \stress{$P$ does not terminate}:

\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.5cm,
                    semithick]
\node[initial,state] (A) {$x=0$};
\path (A)  edge [loop above] node {} (A);
\end{tikzpicture}
\end{frame}

\subsection{Abstraction refinement}
\begin{frame}{Abstraction refinement}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
                    semithick]
%\tikzstyle{every state}=[fill=red,draw=none,text=white]

  \node[state] (A)              {$A$};
  \node[initial, state] (B) [below of=A] {$B$};
  \node[state]         (C) [right of=B] {$C$};
  \node[state]         (D) [right of=C] {$D$};
  \node[state]         (E) [right of=D] {$E$};
  \path (A) edge node {} (B)
        (B) edge node {} (C)
        (C) edge [loop above] node {} (C)
            edge node {} (D)
            edge [bend left] node {} (E);
\end{tikzpicture}

$x' = x+2 \land x \neq 10^{10}$
\bigskip

$E$ is reachable in the abstract and not in the concrete.

Would have been prevented using predicate $x < 10^{10}-1$. Can this be made automatic?
\bigskip

Yes: compute weakest precondition $wp(\neg E)$ for one step: $x \leq 10^{10} \land x+2 \leq 10^{10} \equiv x \leq 10^{10}-2$.

Add $x \leq 10^{10}-2$ as predicate and voilą.
\end{frame}

\begin{frame}{CEGAR}

Counterexample guided abstraction refinement
\bigskip

Generalize the idea «\,compute weakest precondition and add predicates\,».
\end{frame}

\begin{frame}{Some tools}

\begin{itemize}
\item Bounded model checking on C programs: CBMC
\item Predicate abstraction on C programs: Microsoft Device Driver Verifier [SLAM], BLAST
\item SMT-solvers: Yices (SRI), Z3 (Microsoft)
\end{itemize}
\end{frame}


\end{document}