Correctness and Incorrectness Reasoning

Let’s say we have a piece of code $C$ which can be executed using states $s \in S$ as inputs. And let’s say this execution is described by a big-step semantics $\xrightarrow C$ , which is a binary relation on states in $S$ . That is, $s \xrightarrow C s'$ means $C$ can produce output $s' \in S$ on input $s \in S$ .

There are two approaches to reasoning about the behavior of $C$ . The first one is to defend it: prove that only correct executions exist. Failing to prove correctness is not the same as proving incorrectness. The second approach is to attack it: try to find incorrect executions to exploit or remove. Failing to prove incorrectness is not the same as proving correctness.

Forward Correctness Reasoning

In forward reasoning, we are given a precondition $P$ , which ranges over subsets $P \in \mathcal P S$ of states, and we look for the reachable set of outputs

(1) $\begin{align*} \textup{post}_\exists(C,P) = \{s' \in S \mid \exists s \in P \,.\, s \xrightarrow C s'\} \end{align*}$

that it can produce. This is also known as the strongest postcondition, but we will call it the reachable postcondition of $P$ . It is just the (flattened) image $\llbracket C \rrbracket P$ of $P$ through $\llbracket C \rrbracket$ , where the function $\llbracket C \rrbracket \colon S \to \mathcal PS$ is defined as $\llbracket C \rrbracket s = \{ s' \in S \mid s \xrightarrow C s'\}$ .

The word strongest in the term strongest postcondition historically comes from Hoare logic, where one proves triples $\{P\} C \{Q\}$ . Such a triple asserts that any output of the program $C$ resulting from an input in $P$ must be in $Q$ . Formally, $\llbracket C \rrbracket P \subseteq Q$ , or, equivalently,

$\begin{align*} \label{eq:hoaretriple} \forall s \in P \,.\, \forall s' \in S \,.\, (s \xrightarrow C s' \implies s' \in Q),\end{align*}$

In Hoare logic, postconditions can be arbitrarily weakened. If $\{P\} C \{Q\}$ and $Q \subseteq Q'$ , then surely $\{P\} C \{Q'\}$ . Moreover, $\{P\} C \{\top\}$ is always valid for any $C$ and $P$ . Here, $\top$ denotes true, or the whole statespace $S$ . Indeed, $\llbracket C \rrbracket P \subseteq S$ always.

For correctness reasoning purposes, proving $\{P\} C \{Q\}$ with a postcondition $Q$ that is weaker than the strongest postcondition is OK, as long as $Q$ describes only safe states, or good states. The strongest Hoare postcondition of $P$ , i.e., the Hoare postcondition that provides the most information, is given by

$\begin{align*} \textup{strHoarePost}(C,P) = \bigwedge_{Q \in \mathcal P S} \big\{ Q \mid \{P\} C \{Q\} \big\}. \end{align*}$

Clearly, $\{P\} C \{\textup{strHoarePost}(C,P)\}$ , and if $\{P\} C \{Q\}$ , then $\textup{strHoarePost}(C,P) \subseteq Q$ , that is, $\textup{strHoarePost}(C,P)$ is indeed the strongest Hoare postcondition. Moreover, $\textup{strHoarePost}(C,P) = \textup{post}_\exists(C,P).$ That is, the strongest Hoare postcondition is equal to the reachable postcondition we are looking for—the set of all outputs reachable from $P$ .

Forward Incorrectness Reasoning

The Hoare postcondition $Q$ in a Hoare triple $\{P\} C \{Q\}$ overapproximates the postcondition (1) in Hoare logic. In O’Hearn’s recent description of incorrectness logic¹, on the other hand, the reachable postcondition is underapproximated.

An O’Hearn triple $[P] C [Q]$ asserts that $\llbracket C \rrbracket P \supseteq Q$ . This is an offensive approach where we are trying to find bad states in $Q$ . If there aren’t any, then there is no guarantee of safety. But if there are, well, at least we found a bug.

The word strongest in the traditional term strongest postcondition is no longer appropriate in the context of incorrectness logic. Indeed, in incorrectness logic, postconditions can be arbitrarily strengthened, and weaker postconditions provide more information; more possibly bad states. So let’s define the weakest O’Hearn postcondition given a precondition $P$ as

$\begin{align*} \textup{wkOHearnPost}(C,P) = \bigvee_{Q \in \mathcal P S} \{ Q \mid [P] C [Q]\}. \end{align*}$

Theorem. Let $C$ and $P$ be given. For all $Q,R \in \mathcal P S$ such that $\{P\} C \{Q\}$ and $[P] C [R]$ :

$R \subseteq \textup{post}_\exists(C,P) = \textup{wkOHearnPost}(C,P)$ ; and
$Q \supseteq \textup{post}_\exists(C,P) = \textup{strHoarePost}(C,P)$ .

Backward Correctness Reasoning

Given a set $Q$ that describes safe outputs, it can be interesting to find the set of inputs

(2) $\begin{align*} \textup{pre}_\forall(C,Q) = \{ s \in S \mid \forall s' \, . \, s \xrightarrow C s' \implies s' \in Q\} \end{align*}$

for which all possible outputs are safe, i.e., lead to $Q$ . This set is sometimes called the weakest precondition (in partially correct Hoare logic) or the weakest liberal precondition, but we will call it the safety precondition of $Q$ . Indeed, this definition uses universal quantification to guarantee safety with the precondition; in contrast, the reachable postcondition (1) uses existential quantification (taking the image).

In practice, one finds a precondition $P$ that is sufficiently safe for $Q$ . This means that $P$ may exclude certain inputs that are safe to use (false negatives). This is mainly due to the possible presence of loops or (recursive) function calls.

In Hoare logic, sufficiently safe means approximating the safety precondition from below. Indeed, preconditions in Hoare triples can be arbitrarily strengthened (if $\{P\} C \{Q\}$ and $P' \subseteq P$ , then surely $\{P'\} C \{Q\}$ ), and weaker preconditions (more inputs) provide more information. Moreover, $\{\bot\} C \{Q\}$ is always valid for any $C$ and $Q$ . Here, $\bot$ denotes false, or the empty set of states.

Given $Q$ , the weakest Hoare precondition, is defined as

$\begin{align*} \textup{wkHoarePre}(C,Q) = \bigvee_{P \in \mathcal P S} \big\{ P \mid \{ P \} C \{ Q \} \big\}.\end{align*}$

Theorem. Let $Q$ and $C$ be given. For all $P \in \mathcal P S$ such that $\{P\} C \{Q\}$ , we have

$P \subseteq \textup{wkHoarePre}(C,Q) =\textup{pre}_\forall(C,Q) .$

Backward Incorrectness Reasoning

Now using your advanced intuition for duality, looking at the theorem above about forward postcondition reasoning, we should be able to define the strongest O’Hearn precondition in incorrectness logic. Indeed, preconditions in O’Hearn reasoning can be arbitrarily weakened: if $[P] C [Q]$ , meaning $\llbracket C\rrbracket P \supseteq Q$ , and we have $P \subseteq P'$ , then surely $[P'] C [Q]$ . However, although $\{\bot\} C\{Q\}$ is always valid, it need not be the case that $[\top] C [Q]$ is valid. This would namely mean that $\llbracket C \rrbracket^{-1}S \supseteq Q$ for all $Q$ , but this is not true: some outputs may not be reachable.

The strongest O’Hearn precondition is defined as

$\textup{strOHearnPre}(C,Q) = \bigwedge_{P \in \mathcal PS} \{ P \mid [P] C [Q] \}.$

The strongest O’Hearn precondition is generally speaking not comparable to the weakest Hoare precondition. In fact, it cannot be shown that $[P^*] C [Q]$ if $P^* = \textup{pre}_\forall(C,Q)$ . Indeed, one would be obliged to show that $Q \subseteq \llbracket C \rrbracket P^*$ . But taking arbitrary $s' \in Q$ , we are not guaranteed to have an $s$ that reaches $s'$ . Intuitively, this is because the set $\textup{pre}_\forall(C,Q)$ uses universal quantification, whereas $\textup{post}_\exists(C,P)$ used existential quantification. In summary:

In Hoare logic, $\{P\} C \{Q\}$ iff $\llbracket C \rrbracket P \subseteq Q$ ; we can approximate the safety precondition from below and the reachable postcondition from above.
In incorrectness logic, $[P] C [Q]$ iff $\llbracket C \rrbracket P \supseteq Q$ ; we can approximate the reachable postcondition from below, but we can not approximate the safety precondition from above.

But if you think this is the end of the story, you are in for a treat.

Backward Incorrectness Reasoning Again

The fact of the matter is that Hoare triples $\{P\}C\{Q\}$ describe sufficiently safe preconditions $P$ for $Q$ : the precondition $P$ may exclude certain inputs that should actually be considered safe, i.e., leading to $Q$ . These can be called false negatives.

If, in the offensive spirit of incorrectness reasoning, we try to find a precondition for $Q$ as a set of unsafe states, however, knowing that $P$ is sufficient for $Q$ is not what we want. Indeed, it would be enough to know that there is an output in $Q$ reachable from $P$ . That is, we are not chasing the safety precondition $\textup{pre}_\forall(C,Q)$ as defined in (2), but we are chasing the reaching precondition

(3) $\begin{align*} \textup{pre}_\exists(C,Q) = \{s \in S \mid \exists s' \in Q \,.\, s \xrightarrow C s' \}\,,\end{align*}$

that is, the preimage of $Q$ . If we find this set of inputs, knowing $s \in \textup{pre}_\exists(C,Q)$ , with $Q$ a set of bad states, we know for sure that $s$ has a bad output.

There is a duality between $\textup{pre}_\forall(C,Q)$ and $\textup{pre}_\exists(C,Q)$ , which is a direct consequence of the duality between existential and universal quantification:

Lemma. For all predicates $Q \in \mathcal P S$ :

(4) $\begin{align*} \textup{pre}_\forall(C,\neg Q) = \neg\textup{pre}_\exists(C,Q)\,. \end{align*}$

As we argued above, the safety precondition $\textup{pre}_\forall(C,Q)$ can be approximated only from below. But like the reachable postcondition, the reaching precondition $\textup{pre}_\exists(C,Q)$ can also be approximated from below as well as from above, due to the existential quantification. For this, we use the following definitions:

Definition (Cousot triple). A Cousot triple $(P) C (Q)$ asserts that $\llbracket C \rrbracket^{-1} Q \subseteq P$ , i.e.,

$\forall s' \in Q \,.\, \forall s \,.\, s \xrightarrow C s' \implies s \in P.$

Preconditions of Cousot triples can be arbitrarily weakened, and we have $(\top) C (Q)$ always. Define the strongest Cousot precondition as

$\textup{strCousotPre}(C,Q) = \bigwedge_{P\in\mathcal P S} \{ P \mid (P) C (Q) \}$

Definition (Ascari triple). An Ascari triple $\langle P\rangle C \langle Q\rangle$ asserts that $\llbracket C \rrbracket^{-1} Q \supseteq P$ , i.e.,

$\forall s \in P \,.\, \exists s' \in Q \,.\, s \xrightarrow C s'.$

Preconditions of Ascari triples can be arbitrarily strengthened, and we have $\langle \bot \rangle C \langle Q \rangle$ always. Define the weakest Ascari precondition as

$\textup{wkAscariPre}(C,Q) = \bigvee_{P\in\mathcal P S} \{ P \mid \langle P\rangle C \langle Q\rangle \}$

I named Cousot triples after Cousot & Cousot, who first described necessary preconditions², and Ascari triples after the main author of the paper³ describing sufficient incorrectness logic.

Theorem. Let $C$ and $Q$ be given. Let $P,R \in \mathcal P S$ be such that $\langle P \rangle C \langle Q \rangle$ and $(R) C (Q)$ . Then

$P \subseteq \textup{pre}_\exists(C,Q) = \textup{wkAscariPre}(C,Q)$ ; and
$R \supseteq \textup{pre}_\exists(C,Q) = \textup{strCousotPre}(C,Q)$ .

To find errors, it is much more compelling to use Ascari triples (sufficient incorrectness logic). With a bad postcondition, your precondition is guaranteed to have a bad execution, which is not the case for Cousot triples, since they overapproximate. This is why Ascari et al. call their new logic sufficient incorrectness logic: the preconditions you find are sufficiently incorrect.

There is the following neat correspondence between Cousot triples and Hoare triples, which resembles the duality in the Lemma (4) above between the reaching precondition and safety precondition:

Theorem. For all predicates $P,Q \in \mathcal P S$ : $\{\neg P\} C \{ \neg Q\}$ if and only if $(P) C (Q)$ .

I only show $\implies$ . The goal is to show that $\llbracket C \rrbracket^{-1} Q \subseteq P$ , or, equivalently, that $\neg P \cap \llbracket C \rrbracket^{-1} Q = \emptyset$ . Let $s\in \neg P$ and suppose also $s \in \llbracket C \rrbracket^{-1} Q$ . Then there is $s' \in Q$ such that $s \xrightarrow C s'$ . This contradicts $\{\neg P\} C \{\neg Q\}$ . □

It is tempting to conjecture that also $[P] C [Q]$ if and only if $\langle \neg P \rangle C \langle \neg Q \rangle$ . This is not true in general however, due to existential quantification. Indeed, suppose $[P] C [Q]$ , i.e., $\llbracket C \rrbracket P \supseteq Q$ . In this situation, it is still possible that there is an $s'$ in $Q$ reachable from some $s$ not in $P$ that does not reach into $\neg Q$ . That is, nothing about this guarantees $\neg P \subseteq \llbracket C \rrbracket^{-1} \neg Q$ . The following picture should make this clear:

In this situation, we have $[P] C [Q]$ , but not $\langle \neg P \rangle C \langle \neg Q \rangle$ .

Postconditions Again

For the sake of completeness, we should define the postcondition dual to the reachable postcondition:

$\textup{post}_\forall(C,P) = \{ s' \in S \mid \forall s \,.\, s \xrightarrow C s' \implies s \in P\},$

Frankly, I have no idea why this set could be interesting in the least. Clearly, by duality of existential and universal quantifier, we have the following:

Lemma. Let $P \in \mathcal P S$ be a predicate. Then $\textup{post}_\exists(C,\neg P) = \neg \textup{post}_\forall(C,P)$ .

Postconditions in Cousot triples can be arbitrarily strengthened, and we always have $(P) C (\bot)$ . Postconditions in Ascari triples can always be weakened, but we do not necessarily always have $\langle P \rangle C \langle \top \rangle$ , because we do not know if all outputs are reachable.

We can approximate the dual postcondition from below using Cousot triples, by defining

$\textup{wkCousotPost}(C,P) = \bigvee_{Q \in \mathcal P S} \{ Q \mid (P) C (Q) \}$

We then have:

Theorem. Let $C$ and $P$ be given. Let $Q \in \mathcal P S$ be such that $(P) C (Q)$ . Then

$Q \subseteq \textup{wkCousotPost}(C,P) = \textup{post}_\forall(C,P)$

We can attempt to approximate the dual postcondition from above by using Ascari triples, by defining

$\textup{strAscariPost}(C,P) = \bigwedge_{Q \in \mathcal P S} \{ Q \mid \langle P \rangle C \langle Q \rangle \}$

Like with the safety precondition, however, this fails again due to universal quantification.

In summary:

In Hoare logic, $\{P\} C \{Q\}$ iff $\llbracket C \rrbracket P \subseteq Q$ ; we can approximate the sufficient precondition from below and the reachable postcondition from above.
In incorrectness logic, $[P] C [Q]$ iff $\llbracket C \rrbracket P \supseteq Q$ ; we can approximate the reachable postcondition from below, but we can not approximate the sufficient precondition from above.
With necessary condition triples, $(P) C (Q)$ iff $\llbracket C \rrbracket^{-1}Q \subseteq P$ ; we can approximate the reaching precondition from above and the dual postcondition from below.
With sufficient incorrectness triples, $\langle P \rangle C \langle Q \rangle$ iff $\llbracket C \rrbracket^{-1} Q \supseteq P$ ; we can approximate the reaching precondition from below, but we can not approximate the dual postcondition from above.

O’Hearn, P. W. (2019). Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL), 1-32.
Cousot, P., Cousot, R., Fähndrich, M., & Logozzo, F. (2013, January). Automatic inference of necessary preconditions. In International Workshop on Verification, Model Checking, and Abstract Interpretation (pp. 128-148). Berlin, Heidelberg: Springer Berlin Heidelberg.
Ascari, F., Bruni, R., Gori, R., & Logozzo, F. (2023). Sufficient Incorrectness Logic: SIL and Separation SIL. arXiv preprint arXiv:2310.18156.

Correctness and Incorrectness Reasoning

Forward Correctness Reasoning

Forward Incorrectness Reasoning

Backward Correctness Reasoning

Backward Incorrectness Reasoning

Backward Incorrectness Reasoning Again

Postconditions Again

Comments

Leave a reply!Cancel reply

More posts

Performing a DoS attack on my own laptop

Buffer Overflows