1
2
3
4
5
6
graph LR;
	A(Incorrectness logic <br/> A novel concept) --> B(Incorrectness separation logic <br/> Incorrectness logic + Separation logic <br/> Tool: Pulse);
	B(Incorrectness separation logic <br/> Incorrectness logic + Separation logic <br/> Tool: Pulse) --> C(Concurrent Incorrectness separation logic <br/> Incorrectness separation logic + Concurrent separation logic);
	B(Incorrectness separation logic <br/> Incorrectness logic + Separation logic <br/> Tool: Pulse) --> D(Finding real bugs in big programs <br/> Tool: Pulse-X);
	E(Checking data race / OOPSLA 2018 <br/> Tool: RacerD 2018) --> C(Concurrent Incorrectness separation logic <br/> Incorrectness separation logic + Concurrent separation logic);
	F(Checking deadlock / ASE 2021 <br/> Tool in Facebook ) --> C(Concurrent Incorrectness separation logic <br/> Incorrectness separation logic + Concurrent separation logic);

Any gaps exist?

1
2
graph LR;
	A(Iris<br/>) --> B(Diaframe <br/> Automated? Verification of Fine-Grained Concurrent Programs in Iris);

Corresponding paper:

Incorrectness Logic (POPL 2020)

Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic (CAV 2020)

Although such tools intuitively share ideas with correctness-based compositional analyses, the existing foundations of correctness-based analyses do not adequately explain what these bug-catchers do, why they work, or the extent to which they work in practice. A notable such example is the relation between separation logic (SL) and Infer.

Concurrent Incorrectness Separation Logic (POPL 2022)

Finding Real Bugs in Big Programs with Incorrectness Logic (OPASLA 2022)

Pulse: Memory and lifetime analysis

Using it to detect memory safety bugs, namely null-pointer-dereference and use-after-free bugs.

Pulse is an inter-procedural memory safety analysis. Pulse can detect, for instance, Null dereferences in Java. Errors are only reported when all conditions on the erroneous path are true regardless of input. Pulse should gradually replace the original bi-abduction analysis of Infer.

RacerD: Thread safety analysis (Not based on separation logic’s formalism)

RacerD finds data races in C++/Objective C and Java code. This analysis does not attempt to prove the absence of concurrency issues, rather, it searches for a high-confidence class of data races.

There are many types of concurrency issues out there that RacerD does not check for (but might in the future). Examples include deadlock, atomicity, and check-then-act bugs (shown below). You must look for these bugs yourself!

CISL

Inspired by the under-approximate analyses of RacerD and a deadlock detector.

CISL framework: CISLDC (CISL with disjoint concurrency) for detecting memory safety bugs, CISLRD (CISL with race detection) for detecting races on shared memory, and CISL~DD ~ (CISL with deadlock detection) for detecting deadlock scenarios.

CISLSV (sv怎么设计的)

Pulse-X (自动化怎么驱动的)

A new, automatic program analysis for catching memory errors, based on ISL. 15 new real bugs in OpenSSL have been found, which we have reported to OpenSSL.

接下来

CISLSV (sv怎么设计的)

Reasoning about the high-level (abstract) representation of the state

the high-level states are typically modelled by a partial commutative monoid (PCM)

CISLDC for disjoint concurrency, so what about shared concurrency? So using CISLSV

$with_\tau r\ do\ C$ 是 $acq_\tau r; C; rel_\tau$的简略表达

$res_\mathcal{S}^r(\tau:n)$ describes the resources necessary for $\tau$ to acquire $r$ with subvariant $\mathcal{S}$, where $n$ denotes the contribution of $\tau$ on $r$: the number of times $\tau$ has accessed $r$.

SV-CS
$$
\frac{\forall m\geq n. [p\mathcal{S}(m)]\ C\ [ok: q\mathcal{S}(m+1)]\quad stable(p, q)}{[pres_\mathcal{S}^r(\tau:n)]\ with_\tau r\ do\ C\ [ok: qres_\mathcal{S}^r(\tau:n+1)]}
$$

permission: 表示当前线程$\tau$已经访问共享资源$r$的次数$n$。从线程的角度描述它所能访问的共享资源

resource map: 记录了共享资源$r$，被哪个线程$o$所持有，此时的subvariant $\mathcal{S}$，和记录了已经访问该共享资源$r$的线程以及相关次数之间的映射$t$。从共享资源的角度描述

Pulse-X (自动化怎么驱动的)

CSL Family Tree

![image-20230321162541448](D:\Program Files (x86)\Typora\typora-user-images\image-20230321162541448.png)

Some nature idea:

Send / receive concurrency?

Disjoint / shared concurrency get together?

CISL as a parametric framework

can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection

detect that the subset of program behaviours has bugs

  • no well-understood or unifying theory underpinning such under-approximate analyses

  • spend a significant amount of technical effort proving a no-false-positives(NFP) theorem, stating that the bugs found by the tool are indeed real bugs, and such theorem is customized

  • So need a unifying theory that underpins concurrent under-approximate reasoning(for proving incorrectness, i.e. the presence of bugs)

  • ISL only apply to sequential programs and do not support reasoning about concurrent bug catching analyses.

Why “parametric”?

A disturbing trend for each new library or concurrency primitive to require a new separation logic.

CISL allows us to prove triples of the form $[p]\ C\ [\epsilon :q]$, stating that every state in $q$ is reachable by executing $C$ starting in some state in $p$. The $\epsilon$ denotes an exit condition that may be either $\color{green}ok$ to denote normal (non-erroneous) execution, or $\epsilon \in \text{ErExit}$ to denote a buggy (erroneous) execution ($\text{ErExit}$ is supplied to CISL as a parameter to distinguish different classes of bugs such as memory safety errors, races and so forth).

How does the $\text{L}$ come from?

To better track memory safety errors and connect them to culprit instructions, we annotate instructions that may cause such errors with a label $\text{L} \in Label$. As we demonstrate shortly, when an error is encountered we report the label of the offending instruction (e.g. $\text{L}$).

注意一下thread-locality

CISLSV state: triple $s=(l, p, \rho)$, $l\in LState$ is a local state, $p\in Perm$ is a permission and $\rho\in RMap$ is a shared resource map.