# SoK: Guarantees in Software Security

Marcel Böhme
MPI-SP, Germany

# Guarantees in Software Security

Marcel Böhme
MPI-SP, Germany

###### Abstract

We review general approaches to _reason about the security_ of a software
system and reflect upon the _guarantees_ they provide. We introduce a taxonomy
of _fundamental challenges_ towards the provision of guarantees, and discuss
_how these challenges are routinely exploited_ to attack a system in spite of
credible assurances about the absence of such bugs. It is only when we
identify, study, and acknowledge the flaws in our current reasoning systems
today that we can develop effective mitigation strategies in the future. To
this end, we finally propose a research programme whose goal it is to tackle
the software security challenges of this decade.

##  I Introduction

Software security has always been a game of cat and mouse. For instance,
despite the hard work on mitigations and the awesome innovations of the
security team at Apple, for several years, it had never taken longer than a
few weeks from the release of the new iPhone to the development of a
jailbreak.111https://en.wikipedia.org/w/index.php?title=IOS_jailbreaking&oldid=1144416750#By_device_and_OS
A single security flaw (e.g., in a module for keeping logs) can put millions
of citizens at risk [1, 2]. Every attack follows a more sophisticated
mitigation. Every mitigation follows a more sophisticated attack. Will it ever
end? Can software security be solved once and for all?

An _ideal approach_ would _guarantee_ that the system is able to withstand all
possible attacks considered within the threat model. A _practical approach_
will help to prevent, find and fix, or detect and mitigate some security
flaws. Yet, the fact that such a technique does _not detect_ any security
flaws has absolutely no bearing on whether _there exists_ a security flaw that
can be exploited. If no tool sounds an alarm, the unwitting might be under the
impression that their mitigations are effective even though, as we shall
argue, there is _fundamentally_ always a possibility that there exists a
successful attack on the system. How can we find out, which security flaws are
currently missed _despite_ a set of mitigations? What are the precise reasons
_why_ we can never be absolutely sure about the security of a software system?
How do our existing approaches tackle these challenges? And what can we do to
minimize the risk of successful attacks on our systems?

###  I-A Paradise Lost

The first approaches to reason about properties of a program were developed
when the first programming languages were invented. A _programming language_
consists of a set of syntactic and semantic rules that allow developers to
tell the computer precisely what it should do with the available hardware to
process inputs. _Syntactic rules_ determine the structure of a program while
_semantic rules_ determine its behavior.

If the executions of _any_ program are fully decribed by the program’s
instructions and the language rules, why not also reason about program’s
properties rigorously using only those rules? In 1969, Hoare introduced a
formal system with a set of logical rules to reason about a program’s
correctness [3]. He argued that a program can be viewed as a predicate that
describes every relevant observation that can be made of the behaviour of the
computer executing that program [4].

Many logics have been developed, and the field of software verification has
substantially progressed with many success stories. For instance, Project SeL4
develops the first _formally verified OS microkernel_ ”with a full code-level
functional correctness proof” [5]. Project Everest builds a _fully verified
implementation of HTTPS_ , including verified cryptographic libraries [6, 7]
and tools to generate verified parsers [8]. Project CompCert develops the
first _formally verified compiler_ which ”guarantees that the safety
properties proved on the source code hold for the executable compiled code as
well” [9]. These are just some examples of exciting and hugely successful
projects that build critical systems undoubtedly with an _unprecedented degree
of assurance_.

However, not even “formally verified” means “free of bugs or security flaws”.
For instance, in Project CompCert, Kang et al. [10] found a bug in the
formally verified value analysis which was missed due to an under-
specification and another bug in a formally verified helper function which was
missed due to an invalid axiom. In Project SeL4, five years _after_ Murray and
co-authors [11] formally proved information flow security (i.e., that all
information flows via storage channels are only those that the system’s
security policy permits), the Spectre side channel discovered in the CPU
violates the verified property [12, 13]. In a recent editorial, Vardi reflects
on Hoare’s vision: ”In retrospect, the hope for ‘mathematical certainty’ was
idealized, and not fully realistic, I believe” [14].

_So then, what precisely prevents us from making reliable and trustworthy
claims about the correctness or the security of a software system, and what
can we do about it?_

###  I-B Contributions

We argue that any attack exploits _specific_ challenges that _fundamentally_
exist in all our approaches to reasoning about the security of a software
system. In Section II, we introduce our taxonomy of nine challenges that
prevent us from assessing the degree to which a system is able to withstand
all possible hacking attacks. In Section III, we review eleven general
approaches to reason about (or enforce) the security of a software system and
discuss how they tackle (or fail to tackle) some of these challenges. In
Section IV, we propose a research programme for the field of Software Security
that is focussed on addressing the identified challenges of this decade.

##  II Challenges in Reasoning About Security

What prevents us from assessing the degree to which a software system is able
to withstand hacking attacks? Where are our blindspots when reasoning about
security and how can they be exploited by an attacker? Figure 1 gives an
overview.

###  II-A Security Properties as Black Swans

The first key challenge in software security is to know _which_ properties we
need to hold for a system to be secure. Such security properties are like
black swans: If all swans we have ever seen have been white, we may believe
_all swans are white_ —until we see the first black swan. Similarly, we may
not know that a specific security property needs to hold until its absence is
exploited by an attacker.

For instance, Nakamoto’s consensus protocol (Bitcoin) has been formally shown
to _”guarantee safety and liveness”_ [15]. However, there is nothing
preventing malicious participants from violating their part of that protocol
and casting their vote more than once. To account for this, we need a secure
consensus protocol to have another property called _accountable safety_ [16].
Moreover, there is nothing preventing an attacker from creating network
partitions such that the block confirmation procedure cannot be relied upon.
To guarantee safety under network partitions, we need a secure consensus
protocol to have another property called _finality_ [17]. There are many other
properties that need to be satisfied for a consensus protocol to be able to
withstand attacks, some of which we have already found while others remain
unknown until their absence is exploited.

Figure 1: Challenges of Reasoning about Software Security.

Declaring a system as secure is a _universal claim_ that can never be
confirmed despite all evidence in favor [18]. Universal claims, like ”all
swans are white”, follow inductive reasoning from past observations.222Even
for security by deduction (e.g., via software verification) axioms /
assumptions are assumed to be universal by induction from past observations.
However, observing more white swans does _not_ confirm the claim. In the
philosophy of science this is known as the _Problem of Induction_. Universal
claims can only ever be refuted, e.g., by finding at least one black swan.
This is why the Scientific Method requires us to firmly seek to _falsify_ a
new scientific theory (which makes a universal claim) before it can be
accepted [19].

When the Log4J vulnerability was found [1, 2], everyone was rushing to explain
how it could have been found much earlier—easy to say in retrospect. Log4J is
a popular logging framework for Java used in many critical system. If the
attacker can control the text that is logged, they could exploit the (default-
enabled) JNDI feature which enables a user to fetch and load Java objects from
an (attacker-controlled) server. There was a similar vulnerability in the
early days of Internet browsers. Before the same-origin policy was
introduced,333https://developer.mozilla.org/Web/Security/Same-origin_policy
malicious websites could open, e.g., the user’s Gmail website in an invisible
iframe and read all its contents. Recently, a vulnerability was discovered in
Google’s Pixel phone that allowed attackers to recover the original screenshot
(e.g., of a credit card number) when a cropped or redacted version of that
screenshot was shared on the Internet (CVE-2023-21036). Before 2017, no one
anticipated the problematic impact of speculative execution or minor memory
defects [12, 20].

Some program behaviors are vulnerabilities only _in hindsight_ which are
difficult to anticipate beforehand. These examples demonstrate that it is
difficult to know _which_ high-level properties we need to hold for a system
to be secure. We might be absolutely convinced that all swans are white until
we bear witness to the very first black swan.

We can attempt to anticipate certain kinds of attacks by following a
systematic elicitation process. For instance, we can define a _threat model_ ,
i.e., a structured representation of all the information that affects the
security of an application. Some attacks will be considered within the threat
model while others will be considered outside. However, due to ”black swan
properties”, there are always attacks that are not being considered by the
threat model in the first place. This is our first challenge for reasoning
about software security that prevents us from providing a security guarantee.

###  II-B Fidelity of Operationalization

Assuming we know which high-level security properties should hold, the second
key challenge is closing the gap between the immeasurable high-level property
and the measurable, operational definition of that property.
_Operationalization_ is the process of defining the measurement of a
phenomenon which is not directly measurable. Without operationalization, we
have no means to detect violations or reason about these properties, at all.
For instance, we all agree that an attacker should not be allowed to execute
arbitrary code. How to operationalize? We could blocklist specific system
calls that are known to directly or indirectly facilitate arbitrary code
execution.444E.g., strcpy, strcat, sprintf, chown, chgrp, mktemp, exec*,
system, popen. However, this could also block important system calls that are
required for many programs to function properly, and we might forget to block
other system calls that could still be exploited. In fact, there are many
other ways to gain arbitrary code execution instead of system calls.

Because we always need to settle on a _specific_ operational definition of a
high-level property, an attacker may be able to violate the high-level
property while keeping the operationalized version intact. For instance, the
high-level property that was guaranteed by both Sancus [21] and VRASED [22] is
a ”provably secure embedded trusted execution architecture”. However, because
the concrete theorems were under-specified, Bognar et al. [23] were able to
successfully attack the trusted architectures. They identified seven attacker
capabilities that were _not_ formally modelled (i.e., operationalized). The
high-level property that is guaranteed by CompCert is verified compilation
[9], but due to a missed case in the specification, an attacker may exploit
security bugs in the binary if it was compiled from multiple source files
[10]. Generally, flaws in the operationalization of a high-level security
property might allow attackers to launch an attack despite our systematic
reasoning about _our operationalized version of_ that property.

To make matters worse, we are limited by the _language_ that we use to express
the operationalized property. For instance, software verification requires a
formal language to write specifications. Symbolic execution requires a
Satisfiability Modulo Theory (SMT) to encode (and check) assertions on the
symbolic program state. Static analysis requires a logic to reason over
certain properties. If the SMT does not support strings or floating point
arithmetic, or if the logic does not support pointers, heap, or timing,
corresponding properties cannot be encoded. In fact, papers introducing new
side channel attacks often come with their own logic to encode and reason
about new types of attacks [24, 25].

This challenge of operationalization is due to a reduction of a complex,
immeasurable reality to simple, measurable concepts. How do we know that the
operationalized property faithfully represents the high-level property? In a
recent study of researchers’ and learners’ understanding of LTL (Linear
Temporal Logic), Greenman et al. found that the encoding of theorems in
English language as LTL formulas ”was fraught with errors and provides
evidence for a large number of misconceptions” [26]. Even a leading researcher
in the field, Benjamin Pierce, required a full week to understand the
functional correctness proof of SeL4 deeply enough to prepare two lectures
about them in a graduate seminar [27]. Of course, the challenge of
operationalization exists for security-unrelated properties, as well: For
instance, how do we know that verifying our operational definitions of
”fairness” in machine learning systems establishes that an ML model is
_actually_ fair? In the philosophy of mathematics, this is known as the
_Problem of Translation_ : How do we know that the terms _inside_ a proof have
the same meaning as the terms _outside_ [28]?

While we like to interpret an analysis result w.r.t. the high-level security
properties, we can only ever concretely reason w.r.t. their operationalized
version. This is our second challenge for reasoning about software security
which prevents us from providing a security guarantee.

###  II-C Modelling Gap in Reasoning Systems

Assuming we know which security properties should hold and how to best
operationalize them, the third key challenge is closing the gap between the
model of the system (upon which the reasoning system works) and the actual
system as it runs in its natural environment. This includes automated
reasoning systems as well as manual code review and auditing. When we reason
about the security properties of a software system, we make certain
_assumptions_ about the running system and _abstract_ away certain details to
simplify the analysis. The fidelity of the model is further reduced by
practical and theoretical limits. In theory, there are questions that we can
ask about a system that are _fundamentally undecidable_ , irrespective of our
reasoning system. In practice, we often sacrifice soundness or completeness
for scalability and efficiency.

As we always reason about a _specific_ model of a software system, an attacker
may be able to violate a security property of the real system while keeping
properties in the model in tact. For instance, the attacker may violate an
assumption of the model, exploit a security flaw at a lower level of
abstraction, or exploit flaws that are missed in the model (e.g., due to
incompleteness). This is our third challenge for reasoning about software
security which prevents us from providing a security guarantee.

####  II-C1 Assumptions

The result of a security analysis must be understood in terms of the
assumptions made, whether implicitly or explicitly. For instance, the security
of cryptographic protocols depends on _assumptions about the computational
resources_ of an attacker or the computational complexity of a mathematical
problem. For example, the RSA public key encryption is secure assuming that we
cannot efficiently factor large numbers into their prime factors. This
assumption is broken on a quantum computer with Shor’s algorithm.
Cryptography, as maturing field with important innovations, has a long history
of make-and-break cycles where assumptions are exploited to break protocols
otherwise shown provably secure [29, 30, 18].

_“Even if a system is secure according to a model, the most common (and
successful) attacks are the ones that violate the model’s assumptions. Over
the years, I have seen system after system defeated by people who thought of
something new”._ _—_ _Dorothy Denning, Nat’l Cyber Security Hall of Fame[30]_

Security guarantees can also depend on _assumptions made about components
outside the model_ that is used to reason about the deployed system. For
instance, Bognar et al. [23] analyzed two provably-secure embedded trusted-
execution architectures [21, 22] and identified nine assumptions, e.g., (i)
Enclave software cannot access unprotected memory or manipulate interrupt
functionality. (ii) Interrupted enclaves can only be resumed once with reti
and not be restarted from ISR. (iii) The dma_addr bus contains the full
address. (iv) All components use a consistent key size. For every assumption,
Bognar et al. demonstrated how it could be exploited to _successfully attack
the trusted architectures_. Kang et al. [10] analyzed the functional
correctness proof of the CompCert verified compiler [9] and identified an
axiom that was empirically invalid and could be exploited such that the
compiled binary would compute a different result than expected from an
analysis of the source code.

_“Successful exploitation is always evidence of someone’s incorrect
assumptions about the computational nature of the system”._ _—_ _Bratus et al.
on “Exploit Programming”[31]_

Assumptions about components outside the model are also made in _language-
based security_. For instance, Rust does not prevent memory corruption
vulnerabilities in calls to unsafe C libraries or when interacting with
hardware (e.g., parsing a stream of
bytes).555https://twitter.com/chompie1337/status/1638306381777235974

Even if assumptions are stated explicitly, it is sometimes difficult to assess
(a) the degree to which an assumption holds for the deployed software system
and (b) the resulting threat to the high-level security guarantee [32, 27,
18].

####  II-C2 Abstraction

A central idea in computer science, _abstraction_ allows us to focus attention
on details of greater importance by removing or generalizing physical,
spatial, or temporal details or attributes of real-world objects or systems.
However, because we must always reason at an (arbitrary but) _specific_ level
of abstraction, an attacker may be able to violate a security property at a
_lower level_ of abstraction even if the property was shown to hold at the
higher level of our model.

There is a well-known gap between a system’s _specification_ and its
_implementation_. Despite demonstrating a security property for the
specification, an attacker might still be able to violate it in the
implementation. For instance, SHA-3 is currently considered as the most secure
cryptographic hash function. Yet, a simple buffer overflow in the most widely
used implementation of SHA-3 allows an attacker to bypass the security by
computing (second) preimages and even to execute arbitrary code on the
victim’s machine [33].

A second well-known gap exists between a system’s _source code_ and its
_compiled executable_. For instance, in the presence of behavior where the
language standard imposes no requirement (i.e., undefined behavior), the
compiler is allowed to do anything it chooses, including ”having demons fly
out of your
nose”.666https://groups.google.com/g/comp.std.c/c/ycpVKxTZkgw/m/S2hHdTbv4d8J
In fact, undefined behavior includes memory safety issues, which currently
constitute 80% of security vulnerabilities exploited in the
wild.777https://googleprojectzero.blogspot.com/p/0day.html Undefined behavior
also includes type confusion vulnerabilities where the same unchanged variable
is interpreted to have different values in different parts of the
program.888https://blog.trailofbits.com/2022/11/10/divergent-representations/
However, even if the compiler guarantees _semantic equivalence_ between source
code and executable, it might be possible to _bypass_ , in the executable,
security properties established at the source level. D’Silva et al. [34]
identified several compiler optimizations, such as dead store elimination,
code motion, and function call inlining that are formally guaranteed to be
semantic preserving but might (i) introduce information leaks through
persistent state, (ii) eliminate security-relevant code, or (iii) introduce
side channels. D’Silva et al. explain that ”the operational semantics used in
correctness proofs includes the state of the program, but not the state of the
underlying machine” [34].

_”Imagine running a formally verified Rust implementation of a provably-secure
protocol on a fleet of CPUs with a microcode bug.”._ _—_ _Marcel Böhme about a
vulnerability in AMD Zen CPUs[35, 36]_

A third gap exists between the _program_ and the _machine_ executing it. For
instance, even if we can perfectly guarantee the absence of timing side
channels by carefully analyzing the program (binary), an attacker might
exploit processor-specific optimizations or microarchitectural features like
speculative execution to violate the constant time property [12, 25, 37]. Even
if we can guarantee information flow security in the program [5], an attacker
might exploit defective DRAM memory modules (RowHammer) [20, 27] or a bug in
the CPU firmware [36] to leak sensitive information.

_“We do not know how to write real-world programs that can operate on
untrusted hardware. Any tiny, innocent-looking, intermittent and probabilistic
misbehavior can, under current architectures, have disastrous security
implications.” —Thomas Dullien[38]_

We can formalize this gap between the abstract model and the concrete system
using weird machines. The concrete system can inhabit states not represented
in the abstract model. We call as _weird machine_ the mapping
$\alpha:\Phi\rightarrow\theta$ between the state space $\Phi$ of the concrete
system and the state space $\theta$ of the abstract model [31, 39]. Note that
$\Phi$ is _not_ a refinement [40] of $\theta$. We call as _sane states_ all
states $s\in\Phi$ s.t. there exists $t\in\theta$ and $t=\alpha(s)$. We call as
_transatory states_ all states $s^{\prime}\in\Phi$ on the (sane-free) path
between any two sane states $s_{1}$ and $s_{2}$ if there exists a path from
$\alpha(s_{1})$ to $\alpha(s_{2})$. _Weird states_ are all other states in
$\Phi$, neither sane nor transatory but unintended. The objective of the
attacker is to move the program into a weird state that can be exploited. From
the attacker’s perspective, the user input is a program for the weird machine.
Vanegue [41] constructs an axiomatic semantics to reason about weird machines
and shows how even programs with proof-carrying code can be exploited by
”programming” the weird machine.

_“The IFSM [Intended Finite State Machine] can only reach a well-defined and
safe set of states. The weird machine on the other hand has a state space of
unknown size that can be explored by ‘programming’ it – sending careful
crafted inputs.” —Thomas Dullien[39]_

The analysis only of an abstract model of the system prevents us from
providing guarantees about the deployed software system. Or as Balakrishnan
and Reps put it: ”What you see is not what you execute” [42]. The specific
level of abstraction is often fixed by the language (or logic) that is used in
the reasoning framework.

####  II-C3 Non-Universal Claims

Approaches like fuzzing, software testing, symbolic execution, runtime
verification, or incorrectness logic only allow us to reason about an
(observed) subset of all executions. Even if we assume that we know which
security properties should hold and how to operationalize them, these
approaches do not allow us to make universal claims about the operationalized
properties. For instance, despite years of fuzzing the Suricata open-source
intrusion detection and prevention system, a one-line division-by-zero bug
that could cause denial-of-service was found only by a careful manual
audit.999https://twitter.com/catenacyber/status/1646860408014118913

####  II-C4 Fundamental Limits

Apart from the gap between the model and the actual softtware system, the
reasoning system itself is often limited in providing any form of guarantees.
For instance, we know that for any sufficiently complex deductive system that
is consistent, there are always true statements that cannot be proved in that
system (Gödel’s incompleteness theorem).

To remain practical, we design over- or under-approximate analyses. An over-
approximate analysis (e.g., abstract interpretation) reports security flaws
that do not exist while an under-approximate analysis (e.g., symbolic
execution) misses security flaws that do exist. We know that all non-trivial
semantic properties of programs are undecidable (Rice’s theorem). For
instance, we know that there exists no algorithm that, in general, could
decide whether two pointers point to the same memory address for an execution
[43, 44]. We also know that there exists no algorithm that, in general, could
detect malware [45].

_“We show that, for languages with if statements, loops, dynamic storage, and
recursive data structures, intraprocedural may alias is not recursive (i.e.,
is undecidable) and that intraprocedural must alias is not recursively
enumerable (i.e., is incomputable) even when all paths in a program are
executable.” — _”Undecidability of Static Analysis” by Landi[43]_ _

Now, theoretical limits have never stopped us from making progress in
practice. However, security is a universal claim, and we cannot be sure about
the degree to which our heuristic choices impact the analysis result. Even if
our procedure is sound, there are properties which we cannot demonstrate for
some program. This prevents us from providing guarantees about a deployed
software system. Worse, we currently do not even know how to _quantify_ the
loss of guarantee [46].

###  II-D An Infinite Regress of Trust

Both, the software and the reasoning systems are realized using components
that we need to _trust_ in a very human sense. We trust the person or tool
conducting the verification (i.e., analysis / check) of the security
properties to be non-malicious. We trust the compiler to be non-malicious. In
fact, we trust an entire stack of components with which our system interacts
(libraries, operating system, hypervisor, hardware, etc). However, this trust
may not be warranted.

For instance, we trust the compiler, particularly when we compiled it
ourselves. In his Turing award lecture [47], Thompson presents a process to
create an open-source compiler that can stealthily inject vulnerabilities into
the compiled binary: In Stage 1, we write a compiler that can compile itself.
In Stage 2, we add code to inject a vulnerability into the compiled binary and
itself into the compiler binary. Then, we recompile the compiler. In Stage 3,
we remove the offending code from the open-source compiler, recompile, and
distribute the resulting compiler binary. The compiler binary will eternally
inject the vulnerability-injecting code when compiling its own vulnerability-
free source. This is Thompson’s reflection on the trust we put into our tools
and the people writing these tools [47]. Of course, we also trust the CPU to
interpret the code precisely as specified [48, 49].

_“The moral is obvious. You can’t trust code that you did not totally create
yourself. [..] No amount of source-level verification or scrutiny will protect
you from using untrusted code”._ _—_ _Ken Thompson’s 1983 Turing Award
Lecture[47]_

On the one hand, we trust the process of generating assurance (from informally
by a person to formally by verifier). For instance, maintainers of critical
open source projects rely on a sophisticated code review process to check the
absence of bugs in new contributions. This being a socio-technical process,
there are opportunities for an attacker to exploit the developer’s trust in
code contributions and inject vulnerabilities that could later be exploited
[50]. Of course, we must assume a priori that the vast majority of
contributions are indeed benign.

Even if we use automated tooling to generate assurance, e.g., formal
verification, we trust that tooling [51]. For instance, even if the
verification tool is trustworthy, critical bugs in its dependencies, such as
the constraint solver [52, 53] may undermine the provided guarantee. In
fuzzing, we may trust the sanitizer to identify all memory safety issues [54].
We may trust that the eBPF verifier101010eBPF (https://eBPF.io) enables users
to instrument a running system by loading small programs into the operating
system kernel. It is used, e.g., to implement security policies. thoroughly
checks user-provided code before it is run in the Linux kernel. However,
despite the verification of the verifier code [55], many security
vulnerabilities have recently been found [56], raising serious concerns
whether this verifier approach is tenable, at all [57].

On the other hand, we trust the assurances that are provided by those tools.
For verfication, Murray and Oorschot [27] compare the user’s interpretation of
the formal guarantees to reading the fineprint in legal contracts. The
fineprint often consists of many pages written in legalese detailing the
specific terms and conditions. Due to the complexity, fineprint is often
readily accepted by non-experts. Consider this: If it takes an expert a week
to understand the correctness proof of SeL4 [27], how can we expect that a
non-expert understands the fineprint of the verification result?

In epistemic philosophy, this is the problem of _Infinite Regress_ : A belief
is justified because it is based on another belief that is justified. We must
anchor our trust somewhere. While these trust anchors are often well-defined
in security-critical software systems, the guarantee of security of a trust
anchor is itself _not exempt_ from all the challenges we so emphatically seek
to expose in this paper. Hence, this infinite regress is a challenge that
prevents us from providing guarantees about the software system.

###  II-E Competing Points of View

There are many stakeholders in a software system. These stakeholders have
different _perspectives_ on the system that might (often unintentionally) not
include security. Stakeholders often have different _requirements_ for the
software system which are sometimes conflicting with its security.

_“The only person that is paid to actually understand the system from top to
bottom is the attacker. Everybody else is usually paid to understand their
part” — _Thomas Dullien_ [58]_

For instance, while the developer takes a _constructive perspective_ , the
attacker takes an _adversarial perspective_ [59]. On the one hand, the
_developer_ is focussed on continuously creating, realizing, and implementing
new features in the software system. On the other hand, the _attacker_ is
focussed on finding ways to exploit this software system [31, 39, 41]. These
conflicting perspectives must be reconciled. The developer implements with
intention but might realize something that deviates from this intention [60].
This difference between intention and realization can be exploited “to program
the weird machine” [39].

_“For every proprietary product, there is a financial incentive to ship the
most unreliable software that cannot be detected as unreliable”._ _—_ _Thomas
Dullien_  _[_38]

Competing points of view might result in stakeholder requirements that
conflict with security.

  * •

The _vendor_ cares about time-to-market where the software system is tested in
production and new features are deployed almost instantly.

  * •

The _customer_ cares about a low cost. In fact, Woods [61] suggests if buyers
cannot distinguish secure from insecure product, then there is incentive to
sell insecure products. Software security exists within a _lemons market_
[62].

  * •

The _user_ cares about performance and a nice user experience, such that the
performance overhead of certain security measures is considered impractical.

  * •

The _developer_ cares about understanding the source code, such that certain
side effects to make code more secure (e.g., more verifiable) are not
appreciated [27, 63, 30].

When developing and advocating our software security tooling and processes, we
should always consider the different stakeholders and their (potentially
competing) perspectives. However, in general competing requirements
practically prevent us from providing guarantees about the software system.

###  II-F Unreasonable Appearance of Security

A software system may only _appear_ to be secure. It might seem counter-
intuitive, but a less critical system may _actually_ be more vulnerable than a
more critical one, although the less critical system _appears_ to be perfectly
secure while the more critical one might be known to contain many security
flaws.

Firstly, _security is a function of incentive_. For instance, despite the hard
work on effective mitigations and the awesome innovations of the security team
at Apple, it never took longer than a few weeks from the release of the new
iPhone to develop a jailbreak. The large market for jailbreaks provides a
strong incentive for hackers. Hence, the more critical a software system is
(i.e., the more users it has), the more independent scrutiny this system will
have undergone. In other words, the number of security flaws that are _known_
for this system might be a measure more of its criticality than its
insecurity. If there is no real (or artificial) incentive for anyone to
develop exploits and to report these bugs, we will never know about the true
insecurity of the system _until_ there is incentive. We also note that, due to
this incentive structure, an attacker will always target low hanging fruits
first. Once a mitigation is introduced and adopted to prevent a large class of
security flaws _currently_ exploited, attackers will just move on to the next
low hanging fruit [64].

_“We shall assume that the enemy knows the system being used. [..] Thus, even
when an entirely new system is devised, [..], one must still live with the
expectation of his [i.e., the enemy’s] eventual knowledge”._ _—_ _Claude
Shannon (1949)[65]_

Secondly, not _knowing_ if a system is insecure does _not_ mean the system is
actually secure. In fact, the security of a system should not depend on the
secrecy of its components. If someone is truly determined to expose
vulnerabilities in software they will, regardless of visibility. According to
Kerckhoff’s principle, a system should be secure _even if_ everything about
the system is public knowledge. In fact, security through obscurity just
increases the imbalance between attacker and defender in favor of the
attacker. There is no support or incentive for ethical hackers to discover and
responsibly disclose security flaws. Independent security researchers and
stakeholders are directly prevented from scrutinizing the security of the
system. While defenders need to find and fix all security vulnerabilities, the
well-resourced attacker (better tooling and expertise) just needs to find a
single security flaw [66]. The reputational and financial damage arising from
unknown exploits of security flaws is significantly worse than inviting
responsible disclosure via an open security approach.

Even if a software system is certified to be secure and no known security
flaws exist, the system might still become insecure if there is enough
incentive to develop an attack. A lack of incentive or visibility practically
prevents us from thoroughly assessing the security of a software system. This
is where economic or legal guarantees can help. For instance, a _bug bounty
program_ guarantees that your software system is at least as secure as you
would pay for someone else to report a security flaw in your system [61].

##  III Approaches to Software Security

###  III-A Provable Security

We shall refer to techniques that use the tools of logic, formal methods,
cryptography, and mathematics to derive a formal guarantee about the security
of a software system as _provable security_. The formal guarantee is provided
with respect to specific assumptions and properties explicitly stated within a
given formal framework (e.g., pre- and postconditions expressed within a
theory or logic). The software system itself is also modelled within that
framework. The manual or automatic derivation of the guarantee about the
required properties from the provided assumptions (i.e., the process of proof)
follows the specific rules of the framework.

####  III-A1 Secure-by-construction

Suppose, we are to develop a new software system. How can we ensure _a priori_
that the new system satisfies certain formally defined properties?

_Formal reasoning about the model_. We could create a formal specification of
the system-to-be-implemented and prove the required properties for this
“model”. For instance, cryptography is a large and active field of research
that studies systems that facilitate secure communication in the presence of
adversaries. Cryptographic protocols such as SSL/TLS are at the core of the
functioning Internet. Some cryptographic protocols have been shown _provably
secure_ [29]: If certain assumptions about the adversary’s access to the
system, the adversary’s computational resources, and the hardness of certain
computational tasks are satisfied, then the stated properties of these
protocols are guaranteed. For software systems generally, model checking or
theorem proving are active fields of research to formally prove if explicitly
stated properties hold within a formal model of the system-to-be-implemented.

_Enforcing the model_. To bridge the gap between specification and
implementation, we could formally specify the system-to-be-implemented,
including all its required properties, and let a program synthesis engine
generate a program that satisfies these properties [67]. Program synthesis
from specifications is an active research area that has been further
invigorated by advances in large language models (LLMs).

####  III-A2 Verification Within One Level of Abstraction

Suppose, we are given an existing software system. How can we ensure _a
postiori_ that it satisfies certain properties?

_Formal reasoning about the software_. The first step of software verification
is to parse the system’s code or executable into a corresponding _model of
computation_ using the syntactic and semantic rules of the programming
language. The process of proof (whether manual, interactive, or automatic) is
then executed on this model of computation according to the rules of the
formal reasoning framework. The process of proof doubles as a forcing function
to explicitly list and refine the assumptions and arguments required to
demonstrate a property [18] and already weeds out a number of bugs in the code
_and_ the formalization (i.e., assumptions and properties).111111The process
of proof ”uncovered 144 bugs in early versions of the seL4 kernel, and about
150 issues in each of design and specification” [5]. The finished proof is a
_formal guarantee_ for the model of computation corresponding to the code that
the given properties hold under explicitly stated assumptions.

_Enforcing the property_. If we require that some untrusted code satisfies a
specific set of properties, we can ask the code be submitted for verification
together with the proof of these properties. Only if the properties are
confirmed, the proof-carrying code can be executed [68]. Again, apart from the
formal guarantee, the formalization itself is a forcing function to explicitly
and formally spell out the required properties and to explicitly list the
allowed assumptions.

####  III-A3 Verification Across Several Levels of Abstraction

Suppose, we demonstrated all pertinent properties for the code of the
implemented software system. How can we ensure that these properties are
preserved when lowered in abstraction, e.g., after compiling verified source
code into an executable?

_Preserving the property_. Normally, the compiled program binary might inhibit
states that are not represented in the code because (i) the programming
language semantics might leave some behaviors undefined and (ii) the compiler
might optimize away certain security-relevant side effects [34]. A certified
compiler extends the semantics to be more specific (e.g., CompCert C [9]
extends ISO C 99), disallows other language constructs (e.g., variable-length
arrays) to tackle undefined behavior,and disables certain optimizations to
avoid removing security-critical side effects defined in the program.

| Reasoning Challenge |
---|---|---
Security Approach |  2.1 Black Swans |  2.2 Operationalization |  2.3.1 Modelling Gap . (Assumptions) |  2.3.2 Modelling Gap . (Abstraction) |  2.3.3 Modelling Gap . (Non-Universal) |  2.3.4 Modelling Gap . (Fundam. Limits) |  2.4 Regress of Trust |  2.5 Competing PoV |  2.6 Unreasonable . Appearance
3.1.1 Secure-by-Construction | ✗ | ✗ | ✗ | ✗ | ✓ |  | ✗ | ✗ | ?
3.1.2 Verification (1 Level) | ✗ | ✗ | ✗ | ✗ | ✓ |  | ✗ | ✗ | ?
3.1.3 Verification (2+ Levels) | ✗ | ✗ | ✗ | ✓ | ✓ |  | ✗ | ✗ | ?
3.2.1 Static Analysis | ✗ | ✗ | ✗ |  |  | ✗ | ? | ✓ | ?
3.2.2 Fuzzing / Monitoring | ✗ | ✓ | ? | ✓ | ✗ | ✓ | ? | ✓ | ?
3.2.3 Audits / Bug Bounty | ✓ | ✓ | ✓ | ✓ | ✗ | ✓ | ✓ | ✓ | ✓
3.3.1 Threat Modelling | ✓ | ✗ | ? | ? | ? | ? | ? | ✓ | ✓
3.3.2 Secure SW Engineering | ✓ | ✗ |  ✓/✗ |  ✓/✗ | ? | ? | ? | ✓ | ?
3.3.3 Language-based Security | ✗ | ? | ? |  | ✓ | ✓ | ✗ |  | ?
3.4.1 Sandboxing | ✗ | ? | ✓ | ✗ | ✓ | ✓ |  ✓/✗ | ✓ | ?
3.4.2 Access Control | ? | ? | ? | ? | ✓ | ? |  ✓/✗ | ✓ | ?

Figure 2: How an approach tackles a reasoning challenge: Tackled ( ✓ ). Not
tackled ( ✗ ). Trade-off (). Unrelated ( ? ).

####  III-A4 Reasoning Challenges

There are several benefits of provable security: It requires us to explicitly,
precisely, and formally spell out the operationalized assumptions, the
operationalized properties, and the formal framework used to reason about
these properties. The proof gives a formal and universal guarantee (§2.2.3)
that the property holds within the formal model of the software system if the
assumptions are met.

_“[Proofs] rule out certain categories of attacks or attacks on certain parts
of the protocol.”— _in “Critical Perspectives on Provable Security” by Koblitz
and Menezes[29]_ _

However, as shown in Figure 2, provable security also suffers from several
challenges as identified in Section II. A priori, provable security provides
no help in identifying or operationalizing important high-level properties
that must hold in the presence of an adversary (§2.1 and §2.2). For instance,
an adversary might exploit the lack of properties that we did not know need to
hold. The guarantee depends on the empirical validity of assumptions about the
actual software system. An attacker can focus on invalidating these
assumptions to attack the system (§2.3.1). The provided guarantee holds only
for a formal model of the actual software system whose level of abstraction is
fixed by the formal logic or theory that is used. An attacker can always focus
on invalidating the guarantee at a lower level of abstraction (§2.3.2). This
can be somewhat addressed by ensuring that the pertinent properties are
preserved across different levels of abstraction.121212In Section IV-C, we
will suggest to _explicitly_ consider the process of proof as the main
artifact of the verification process rather than the proof itself. The proof
process is embedded in a feedback loop guided by attacks identified by other
means. In this process, the operationalization, assumptions, and abstractions
are refined by adjusting axioms and properties and adding required concepts to
the formal logic or theory.

Morever, provable security might impose restrictions on the system that might
be unacceptable to some stakeholders (§2.5), such as intolarable computational
resources, reduced performance, disallowed code constructs [9], unreadable
code [27], or tooling that is incompatible with the tool chain. The
fundamental limits of provable security (§2.3.4) can also be tackled as a
trade-off () by disallowing offending code constructs (e.g., loops or
variable-sized arrays). It is interesting to note that the process of proof is
constructive (from a developer’s perspective) rather than adversarial (from an
attacker’s perspective; §2.5). In terms of regress of trust (§2.4), we also
need the formal model, specification, and tooling to be correct in the first
place.

###  III-B Detective Security

We shall refer to (manual or automated) methods that analyze, prope, or test a
software system so as to make non-universal claims about its security as
_detective security_. The main objective of such methods is to identify and
report bugs and security flaws; no promise about the absence of bugs.131313We
note that provable and detectable security have opposing objectives when
reasoning about software security. One seeks to demonstrate _security_ while
the other seeks to demonstrates _insecurity_. We are thus considering these
approaches as _complementary_ rather than competing (cf. Section IV-C).

A central benefit of detective security is that it does not require
stakeholders to take a specific point of view (§2.5). There is limited impact
on the end-user (e.g., via performance losses), the developer (e.g., via
language restrictions), or the vendor (e.g., via slower time-to-market).
Stakeholders need only be reactive instead of proactive. For instance,
automatic bug finders can often be directly integrated into the development
process (e.g., CI/CD pipeline).

####  III-B1 Static Analysis and Symbolic Execution

We call an automatic analysis that proceeds _without executing_ the program as
_static analysis_. We can distinguish syntactic and semantic static analysis
approaches. _Syntactic approaches_ often apply pattern matching to reason
about textual or structural representation of the source code. _Semantic
approaches_ (incl. symbolic execution or separation logic) reason about an
over- or underapproximation of the program’s state space.

Due to undecidability (§2.3.4) [43], static analysis tools might report bugs
that do _not_ exist (false positives) or fail to report bugs that do (false
negatives). Syntactic tools only find bugs that match the given patterns/rules
while semantic tools work on an approximate (§2.3.2) or an incomplete
representation of the state space (§2.3.3). While these challenges cannot be
solved entirely, there are approaches to reduce the false postive/negative
rate. For instance, CodeQL allows to remove noisy and add new rules.
Furthermore, _a priori_ , detection rules are program-independent (§2.1-2).

####  III-B2 Fuzzing, Testing, and Monitoring

We call an automatic analysis that proceeds _by executing_ the software as
_dynamic analysis_. Well known dynamic analysis techniques are testing,
fuzzing, and monitoring [69, 70, 71]. A mechanism that decides if an execution
reveals a bug is called _oracle_. Examples of oracles are manually-written
assertions [72] or auto-generated buffer overflow checks [73].

In contrast to static analysis, dynamic analysis works on the actual, concrete
state space of the program which ensures the fidelity of the
operationalization (§2.2) and avoids the modelling gap due to abstraction
(§2.3.2) or fundamental limits (§2.3.4). The need to write test cases to cover
unusual behaviors also requires the developer to take an adversarial
perspective (§2.5). Whenever a new security flaw is found, developers can
write new fuzz harnesses or regression tests to detect similar bugs in the
future.

However, while reported bugs are always true positives, dynamic analysis is
incomplete (§2.3.3). Nevertheless, it might be possible to make statistical
statements about the population of executions, given only a sample [46, 74].
The problem of identifying the high-level properties that we need to hold for
a software system is explicitly explored as part of the _oracle problem_ [75],
but remains unsolved (§2.1).

####  III-B3 Independent Audits

We call a _manual analysis_ of the software system as an _audit_. An audit can
come from entities with varying levels of independence. In _DevSecOps_ , the
developing team itself audits the code. In _red teaming_ , an independent team
within the same company audits the code. As part of a _pwning competitions_ or
_bug bounty programs_ , independent security researchers audit the code and
report security flaws. Finally, one can always react to vulnerability exploits
discovered in the wild.

An independent manual audit effectively simulates an attacker and hence does
not, _a priori_ , suffer from the many challenges of automated approaches to
software security. Unless artificially limited (e.g., by rules, biases, or
threat models), an auditor has conceptually the same means to write an exploit
as the archetypical hacker. For instance, red teaming, pwning competitions,
and bug bounty programs provide an increased incentive for experts to detect
and responsibly disclose vulnerabilities (§2.5) as violations of high-level
properties that the vendor did not even consider (§2.1, §2.2). By inviting the
public to scrutinize the security of our software, we do not rely on trust
anchors (§2.4) and generate a more realistic reputation of security (§2.6).
The adverserial approach ensures that there is no inherent modelling gap
(§2.3). Of course, manual auditing does not allow us to make universal claims
about the security of the software system (§2.3.4). Still, a successful
exploit can be considered as a counter example to its security [31]. The
manually reported security flaws are addressed and inform the automatic
detection of similar flaws.

In fact, Woods [61] suggests that bug bounty programs (as well as warranties)
provide an _economic guarantee_ for the security of a software system. We
shall add that bug bounties precisely guarantee that the software system is at
least as secure as we promise to pay someone for a successful attack.

###  III-C Preventive Security

We shall refer to techniques that help us avoid introducing security flaws in
the first place as _preventive security_. This includes _software engineering
efforts_ , such as ensuring security best practices or eliciting project-
specific security requirements as well as _programming language efforts_ to
entirely avoid large classes of security faults, such as memory safety issues,
at the OS or programming language level.

####  III-C1 Threat Modelling

By assuming different possible capabilities of an attacker, we can explore
effective strategies to mitigate the corresponding security risk by
counterfactual reasoning. This is called _threat modelling_. For instance, in
the STRIDE threat modelling approach [76], we ask what if attackers could
spoof the identity of another person, tamper with data shown to the user,
repudiate any involvement in malicious activities, disclose confidential
information, initiate a denial of service, or elevate their privilege to gain
unauthorized access? Thus, the software’s security arises as _prevention_ or
_mitigation_ of explicit _attacker capabilities_.

Identifying the required security properties of a system is really at the
center of threat modelling (§2.1). An explicit and possibly public threat
model allows all involved stakeholders to discuss and agree on a shared
perspective on the system’s security which tackles challenges of competing
points of view (§2.5; [77]) and unreasonable appearance of security (§2.6).

####  III-C2 Secure Software Engineering

We call the systematic integration of security as first-order citizen into the
development process as _secure software engineering_ [78]. This includes, for
instance, best practices for security, new tooling for CI/CD, new roles
(DevSecOps, red teams, threat response), and creating disclosure policies or
threat models.

Having security as first-order citizen in the development process, like threat
modelling, allows all involved stakeholders to discuss and agree on a shared
perspective on the system’s security (§2.5, §2.6). Requirements elicitation
for security helps uncover properties required for the system to be secure
(§2.1). However, if the system is designed but does not exist, yet, we can
only reason about some abstraction of the system under certain assumptions
(§2.3.1, §2.3.2) [79].

####  III-C3 Mitigations and Language-based Security

There is preventive security that enforces _general_ security properties from
_outside_ the software system. Properties can be enforced by the programming
language (e.g., memory safety [80]), the compiler (e.g., hardening [81, 73]),
the operating system (e.g., ASLR [82]), or the hardware (e.g., PAC [83]).

_“To date, there have been zero memory safety vulnerabilities discovered in
Android’s Rust code”. — _Jeffrey Vander Stoep[80]__

The implemented mitigations often quell entire classes of bugs. For instance,
memory unsafety accounts for more than 70% of reported vulnerabilities in the
Chrome browser [84] as well as in the iOS, MacOS, [85] and Android [86]
operating systems [87]. Sanitizers [73] are injected by the compiler to crash
memory-corrupting executions. However, the resulting performance overhead is
considered unacceptable in production (§2.5). The Rust programming language
enforces memory safety at the programming language level using the borrow
checker [88].

_“Will I ever rewrite curl in rust? I don’t believe in rewrites, no matter
which language. I believe in replacing code and fixing components gradually
over time. That *could* mean that we have a curl written mostly in rust in 10
years. Or in 20 years. Or not.”_ _—_ _Daniel Stenberg (curl main
developer)[89]_

However, due to competing points of view (§2.5), developers may (mis)use the
unsafe keyword to interface with _memory unsafe_ code. We must still trust in
the supply chain (§2.4). For instance, a recent memory safety bug in the
OpenSSL package for Rust (CVE-2022-3786) may enable remote code execution in
Rust-based software systems using the OpenSSL package. Some maintainers of
critical projects do not feel ready to rewrite in Rust (§2.5). A sanitizer may
not detect _all_ bugs it is supposed to find, either [54] (§2.4).

While mitigating only specific classes of bugs (§2.1), the enforced security
properties are always fully operationalized (§2.2) and hold universally
(§2.3.1-3). Properties that cannot be enforced at compile time can be enforced
at runtime [73], side-stepping the limitations of static analysis (§2.3.4).

###  III-D Reactive Security

We shall refer to techniques that help us limit the damage an attacker can
cause if parts of the software system have already come under an attacker’s
control as _reactive security_. A central concept of reactive security is
_trustworthiness_. Components possibly exploitable are assumed untrusted.

####  III-D1 Sandboxing and Trusted Execution Enviroments

An effective way to envision a software system that might be partially under
attacker control is by drawing concrete trust boundaries. While security
properties must be upheld for the overall system, some processes can be
explicitly assumed to be untrusted (or to be trust anchors).

Sandboxes do not allow untrusted processes _out_ while trusted execution
environments (TEE) do not allow them _in_. A _sandbox_ is a mechanism for
isolating untrusted processes [90]. For instance, we assume that an attacker
can hijack a virtual machine, a mobile app, or a browser tab and leave it to
the sandbox to prevent the attacker from reaching outside the sandbox. A _TEE_
is a trusted, hardware-enabled enclave that ensures that data is stored,
processed and protected securely [91]. For instance, authentication and mobile
financial services are sometimes run in a TEE. Breaking a software system into
mutually distrustful components run with minimal privileges is called
_compartmentalization_ [92].

_“Foreshadow demonstrates how speculative execution can be exploited for
reading the contents of SGX-protected memory as well as extracting the
machine’s private attestation key. [..] It only takes a single compromised SGX
machine to erode trust in the entire SGX ecosystem.”_ _—Jo Van Bulck et
al.__[_93]

While explicitly addressing the issue of trust in the software system (cf.
Fig. 2; §2.4), an attacker might exploit our trust in the tooling that is used
to enforce isolation [94, 95, 96, 97, 98]. In terms of modelling gap, the
reactive approach requires no assumptions and applies to all executions
(§2.3.1, §2.3.3, §2.3.4). However, the isolation between trusted and untrusted
processes may only be enforced on a certain level of abstraction (§2.3.2) and
for known properties (§2.1).

####  III-D2 Segregation and Access Control

The principle that no user should be given enough privileges to misuse a
system on their own is called _segregation_ or the principle of least
privilege [99]. A user’s privileges to access certain data and resources are
determined via _access control_. While the issue of trust is explicitly
addressed, we still trust the tooling to prevent escalation of privilege
(§2.4).

##  IV Research Programme for Software Security

The prevalent philosophy in software security is to demonstrate the
_generality_ of an approach (§3). When a new technique to prove the absence
of, to discover, or to prevent security flaws is introduced, we would deem it
as successful if no security flaw is missed in an evaluation. At this point,
we hope we have convinced the reader that, fundamentally, no such approach
exists. This incomplete, low-level perspective does not do justice to the
fundamental challenges of reasoning about security and a new perspective is
required. A new perspective that accounts for the “make-and-break” cycle
within which most security tooling exists in practice.141414In fact, security
research is subject to the same make-and-break cycle. Cryptographic protocols
are developed and broken all the time. Mitigations are developed and broken.
Systems are formally verified and exploited. A new perspective that asks us to
focus on indentifying and extending the _specific limits_ of an approach
instead of its general capabilities.

We submit, it is not in the general, but only in the specific, that we can
improve the guarantees provided by our tools. If we cannot have guarantees in
software security, we must work to identify the limitations of our tooling
w.r.t. the software systems it is supposed to protect. We must develop tooling
that can be updated to rectify those identified limitations.

Before we start, let’s recall _why_ , fundamentally, we cannot guarantee the
security of a system with absolute certainty. For any sufficiently complex
system, a reasonably incentivized attacker will always find a way:

  * •

(§2.1) to violate an important property of our system that we _don’t yet know_
should need to hold,

  * •

(§2.2) to violate an important _high-level property_ while keeping the
corresponding _operationalization_ in tact,

  * •

(§2.3) to violate an important property of the _deployed system_ even if the
property was carefully checked or even verified for the system’s (formal)
_model_.

  * •

(§2.4) to exploit our _trust_ in our tooling, processes, systems, mitigations,
and other trust anchors,

  * •

(§2.5) to exploit design decisions made to accomodate _non-security
preferences_ of other stakeholders, or

  * •

(§2.6) to exploit the insecurity of software systems that are promised or
_believed to be secure_.

###  IV-A No Guarantees. Now What?

Empirically, does the security of our software systems improve as part of this
eternal cat and mouse game? The good news is, it gets ever more difficult to
write a successful exploit. For instance, while it took no more than a few
weeks from the release of a new iPhone to the first jailbreak two years, ago,
it now takes several months to bypass all the mitigations that have been put
in place [100].

_“If you want to work on [iOS] jailbreaking, I guess, you are too late. There
is too much going on. [..] Earlier, we could just patch the kernel and be done
with it. Now we need to [..] work around every single mitigation and there are
just more and more coming. [..] Eight months, ago, we started preparing this
jailbreak and we already had kernel read/write, but there was still a lot to
do before we could modify user-space apps”._ _—_ _Tihmstar and CoolStar @
NullCon 2022[100]_

Consider fishing as a metaphor for bug finding where the _net_ represents an
automatic approach to security and _fishes_ represent the security flaws. Our
inability to provide an absolute guarantee just means that for any given net,
there might always be fishes that slip through the net. Yet, clearly this does
not undermine the utility of the net. The cost or effort for others to catch
the remaining fish may just not be worth it.

Last year, Dellago et al. [98] published a study of the market for 0-day
exploits between 2016 and 2021.1515150-day exploits use vulnerabilities that
are unknown to the developers. For the four studied operating systems
(Windows, MacOS, iOS, and Android), the number of 0-days observed in the wild
decreased from 2016 to 2018 but increased again until the end of the study
period. For the two investigated exploit brokers, Zerodium and Crowdfence,
exploit prices increased to a maximum in 2019 and have since remained stable
at USD 2.5-3 _million_ for a full exploit chain with persistence on Android or
iOS. Recently, a third broker, Operation Zero, has announced to offer USD 20
_million_ for the same, which Google’s Senior Director of the Threat Analysis
Group, Shane Huntley, took as a good sign that the developed mitigations are
becoming more effective and exploits more
difficult.161616https://twitter.com/ShaneHuntley/status/1706944206521160070
Schechter [101] confirms that higher prices are a signal of more secure
products.

###  IV-B A Philosophy of Software Security

We recall that software security is a universal claim which can never be
confirmed, demonstrated, or proven [18] while a single identified
vulnerability can be taken as undisputable evidence against any claim of
security [31].

As a _philosophy of science_ , Popper [19] proposed the method of
falsification to tackle the problem of induction: The scientific method
requires us to first ”guess” a falsifiable theory, conduct experiments to try
and find evidence _against_ that theory, and only failing to do so, put
forward this theory.

As a _philosophy of maths_ , Lakatos [28] expanded Popper’s method where he
sought to maximize the empirical validity of formal, mathematical claims.
Lakatos demonstrated the heuristic nature of the formal proof process by
providing a string of proofs of a specific mathematical claim about graphs
(Euler’s characteristic), all of which turn out empirically flawed in one way
or another, despite being formally consistent. To explicitly foster this
heuristic process of formalization and formal proof, Lakatos proposed the
method of _proof and refutation_ which follows a prove-and-break cycle.

_“For Lakatos, the development of mathematics should not be construed as
series of deductions [..]. Rather, these water-tight deductions from well-
defined premises are the (perhaps temporary) end-points of an evolutionary,
and indeed a dialectical, process in which the constituent concepts are
initially ill-defined, open-ended or ambiguous but become sharper and more
precise in the context of a protracted debate.”_ _—_ _Musgrave and Pigden
(Stanford Encyclopedia of Philosophy)[102]_

In this paper, we propose a _philosophy of security_ that follows the methods
of Popper and Lakatos. Instead of developing techniques for security that are
meant to be universal or general, we propose to focus instead on developing
approaches to find evidence _against_ the generality of a technique, and
approaches to reconcile such evidence by dynamic updates to that technique in
this counterexample-guided manner. For our fishing metaphor, instead of
considering the net to be final, our method suggests the fishermen (not the
“others”) should actively, continuously find fishes that slip through to
determine precisely where and how they can improve the net.

Specifically, inspired by Popper and Lakatos our philosophy of security
suggests the following general method.

  1. 1.

Implement a technique $T$ that ensures the security of a software system $S$.

  2. 2.

Actively find evidence _against_ the security of $S$ despite $T$.

  3. 3.

Patch $S$ and improve $T$ by reconciling the most general version of the
negative evidence with the technique.

  4. 4.

Go to (2).

This is how our method is applied to different approaches to software security
presented in Section III. For _provable security_ , we would first develop and
use the technique $T$ to derive a formal guarantee about the security of a
software system $S$, exploit the identified challenges (incl. invalidating
assumptions) to generate a counterexample $ce$ used to attack $S$ in spite of
$T$, patch $S$ and update $T$ by reconciling $ce$ and restart this process
beginning with the verification using the updated $T$. For _preventive
security_ , like language-based security, we would first develop and deploy
the technique $T$ to prevent exploits of security flaws in software system
$S$, exploit the identified challenges (incl. inconsistent assumptions [103])
to generate a counterexample $ce$ used to attack $S$ in spite of $T$, patch
$S$ and update $T$ by reconciling $ce$ (e.g., by making assumptions consistent
and re-enabling mitigations). For _detective and reactive security_ the
approach is analogous: Use $T$ to test-and-fix S. Find a counterexample $ce$
in $S$ despite $T$, and repair $T$ (and $S$) to account for $ce$. In the next
section, we instantiate this method for software verification within one level
of abstraction.

We effectively suggest to move the community focus _away from_ developing
tooling to ensure the security of a software system _toward_ developing
(feedback-directed) approaches to improve the effectiveness of this security
tooling for a given software system. Only such a vulnerability-guided,
incremental hardening of our security approaches will allow us to tackle the
identified reasoning challenges, as summarized at the beginning of Section IV.

Going forward, we should develop new techniques that explicitly accomodate
this counterexample-guided evolution of our approaches. For instance, we
should invent novel diagnosis and debugging techniques for our approaches that
allow us to pinpoint the precise root cause of their failure to discover or
mitigate a given vulnerability. We need innovative techniques to
programmatically reconcile the discovery of a vulnerability to improve the
approach.

Moreover, we should develop in-vivo approaches that analyze a deployed system
directly as it is running in production in its natural environment to minimize
the required assumptions or abstractions. We should explore hybrid approaches
that marry two or more existing approaches to security to overcome the
individual reasoning challenges. We should develop counterfactual approaches
that allow us to assess the security of a software system under varying
assumptions of attacker control, e.g., of certain software components, of
certain exploit primitives, or bypasses of certain mitigations.

###  IV-C Counterexample-guided Meta Verification

We choose _provable security_ (§III-A) as a case study for the application of
our new method. How can we systematically minimize the modelling gap, identify
unknown but relevant security properties, and improve the operationalization
of those high-level properties? We have previously argued that security is a
_universal claim_ which, like a scientific theory, can never be confirmed but
only be refuted. Hence, we propose to apply the Scientific Method to Provable
Security which requires us to firmly seek to _falsify_ the claim of security
for the _actual software system_ once the proof for the _formal model of the
system_ is completed. Instead of ending with the proof, we propose to embed
the proof process more explicitly into a prove-and-break feedback loop.
Successful attacks on the actual software system serve as counter-examples
that must be systematically reconciled into the formalization. As this
counterexample-guided approach allows us to verify the verification process
itself, we call this approach as “adversarial” verification or counterexample-
guided _meta verification_.171717A related procedure is counterexample-guided
abstraction refinement (CEGAR) [104]. In meta verification, the counterexample
violates the property at the highest level of _refinement_ (i.e., the deployed
system) but not in the abstraction. In CEGAR, it is the other way around: the
counterexample violates the property in the _abstraction_ but may not in a
refinement.

If a critical system can be attacked despite a formal proof of its security,
what then is the utility of provable security? Formally verified software like
SeL4 [5] or CompCert [9] are among the most secure, high-assurance systems to
ever exist. While the process of proof already rids the program of many
bugs,181818See Footnote 11 and Reference [105]. the final proof inherently
excludes large classes of security flaws and provides a precise formal
guarantee. The provided guarantee holds within an explicit formalization and
with respect to precisely stated assumptions and security requirements [18].
Indeed, it is those artifacts whose empirical validity we propose to
systematically scrutinize and harden.

Algorithm 1 Counterexample-guided Meta-Verification

1:Initial software system $S$

2:Initial formalized assumptions $A$ and properties $P$

3:Initial formal framework $F$

4:$\langle S,A,P,F\rangle=\text{{verify}}(S,A,P,F)$

5:$\text{Counterex. }ce=\text{{attack}}(S,A,P,F)$

6:while $ce$ exists do

7: $\langle S,A,P,F\rangle=\text{{reconcile}}(ce,S,A,P,F)$

8: $\langle S,A,P,F\rangle=\text{{verify}}(S,A,P,F)$

9: $ce=\text{{attack}}(S,A,P,F)$

10:end while

11:Verified software system $S$

12:Updated assumptions $A$ and properties $P$

13:Empirically more valid formal framework $F$

Algorithm 1 shows our proposed counterexample-guided meta verification
procedure. We invite the research community to develop systematic approaches
for the individual functions. The procedure starts with the verification of
the software system $S$ in Line 1, using an initial set of assumptions $A$ and
properties $P$ formalized within the logic or theory of the verification
framework $F$.

However, in practice and in our proposed procedure, the verification (i.e.,
the function verify) does _not end with the failure to verify_ , but continues
with systematic adjustments to $S$, $A$, $P$, or $F$ until the verification
finally succeeds (returning an updated set $\langle S,A,P,F\rangle$). Once $S$
is successfully verified w.r.t. $A$ and $P$ within $F$, we suggest to attack
$S$ to identify a security flaw $ce$ that still exists in the actual system
$S$ _despite_ the successful verification of its formal model (Line 2). As
long as we can find successful counterexamples $ce$, we must update the system
and verification artifacts to reconcile the counterexample with the formal
model of the system and re-verify using the updated verification artifacts
(Lines 3–7).

It is interesting to note that meta verification effectively tackles the well-
known argument of De Millo, Lipton, and Perlis [32] against the utility of
automated verification. The authors argue that the validity of a formal proof
is usually derived within a _social process_ , and suggest that automated
verification might remove this social process and thus the means by which to
establish a proof’s validity. Meta verification addresses their argument by
substituting the social process with a programmatic falsification of the
verification result until no more counterexample $ce$ can be found.

####  IV-C1 Verification-guided Vulnerability Discovery

Once the software system has been fully verified, we suggest to try and attack
the software system despite the formal proof of security. Apart from existing
vulnerability discovery techniques (§3.2), we propose to systematically and
perhaps automatically exploit the challenges of formal reasoning about
software security so as to “harden” the formal guarantee, the verification
artifacts, and the software system.

To implement attack, we might identify black swan properties $p\not\in P$ or
exploit an infidelity in the operationalization of some $p\in P$. For any
assumption $a\in A$, we might seek to invalidate $a$ for the actual system
[106, 79]. Given the formal framework $F$, we might seek to violate a property
$p\in P$ for $S$ while keeping $p$ in the abstract model of $S$ in tact. To
increase public _trust_ in tooling and framework $F$, we propose to invite all
stakeholders to subject $F$ itself to bug finding, and to maximize the
layman’s comprehension of the provided formal guarantees (or “fine print”
[27]).

####  IV-C2 Counterexample-guided Reformalization

Once a violation $ce$ of a property $p\in P$ is identified in the deployed
software system $S$ _despite_ the formal guarantees provided by the formal
reasoning framework $F$ modulo the assumptions $A$, we must update the
verification artifacts accordingly. To implement reconcile, we suggest to
identify the verification artifacts $\langle A,P,F\rangle$ that are
inconsistent with the counterexample and systematically and perhaps
automatically update the artifact(s) to enforce a property violation in the
presence of $ce$ for the unchanged $S$. For instance, we might add new
properties to $P$, remove invalid assumptions from $A$, or update the
reasoning framework $F$, e.g., by fixing a bug in the tooling [52] or by
extending the reasoning rules (i.e., logic [25] or assurance cases [107]).
Once the formalization recognizes $ce$, the software system $S$ should be
fixed, re-verified, and attacked until no counterexample can be found (Lines
3–7; Alg. 1).

###  IV-D Automatic Counterfactual Analysis

If we accept that the security of a software system can never be guaranteed,
we must assume that there are security flaws that attackers can exploit.
However, it is never a single bug that allows attackers to achieve their
goals. Instead it is a set of security flaws that are often exploited in a
specific sequence before their goal is reached. In offensive security, these
individual flaws are said to provide _exploit primitives_ [108] towards
special capababilities. The process of chaining these primitives can be taken
as _programming the weird machine_ [31, 39, 41]. When a security flaw—that was
underpinning a working exploit—is fixed, an attacker would only need to find
another security flaw that gives the same primitive or capability to repair
the exploit chain again.

_“Over the last few years Apple has been hardening the Safari WebContent (or
‘renderer’) process sandbox attack surface on iOS, recently removing the
ability for the WebContent process to access GPU-related hardware directly [as
a mitigation]. Access to graphics-related drivers is now brokered via a GPU
process which runs in a separate sandbox. Analysis of this in-the-wild exploit
chain reveals the first known case of attackers exploiting the Safari IPC
layer to ‘hop’ from WebContent to the GPU process, adding an extra link to the
exploit chain [as a bypass].”_ _—_ _Ian Beer (Google P0) on an in-the-wild
0-day iOS exploit chain[109]_

We believe that an effective approach to security explores security risks and
priorities by _automatic counterfactual reasoning_ : “What if the attacker had
the capability to …?” (e.g., read 4 bytes from this address, bypass this
mitigation, hijack this component, or access the Internet). Such a
counterfactual analysis does not require us to develop the technology for an
actual bypass. Instead, we propose to develop automatic security analysis
techniques that analyze the system _assuming_ the attacker had a certain
capability (for different capabilities).

_“So the answer to ‘is this bug exploitable or not?’ is often just ‘yes,
because the bug is in a known exploit equivalence class’. It can be as simple
as: ‘this is exploitable because the primitive you get is just like the one in
oob_timestamp.c, but you need B. Azad’s new PAC bypass as well’”._ _—_ _Ben
Hawkes (former Lead of Google P0)[108]_

This counterfactual security approach has a number of advantages. Firstly, it
helps us focus on larger _exploit equivalence classes_ [108] and their
mitigations instead of individual bugs and their fixes. Secondly, it helps us
understand the degree to which the system’s security relies on trust anchors
and mitigations to be trustworthy. Thirdly, it helps us to _build for
insecurity_ by reasoning beyond the initial attack surface and planning and
adding more fail-safes later in a prospective exploit chain. Lastly, this
counterfactual security approach operationalizes and automates threat
modelling at the level of source code.

## Acknowledgments

This paper was written out of a deep interest to understand the types of
guarantees that our approaches to software security provide _fundamentally_
and how we should develop the next generation of approaches if we accepted
that there are no guarantees to begin with. On the one hand, researchers
generate promises of guarantees and effectiveness that are broken time and
again. On the other hand, practitioners are troubled by the obvious lack of
guarantees, and that we have absolutely no sound means to measure just how
effective our techniques are. This paper is an attempt to shed some first
light and to reconcile the promise with reality.

I would like to thank the members of my group, my colleagues, and my friends
who, in the last five years, have listened to my thoughts on this topic, read
my initial drafts, and provided invaluable feedback and ideas for this paper.
Special thanks go to Toby Murray, Joshua J. Drake, Daniel Woods, and Thomas
(Halvar Flake) Dullien for the insightful feedback and inspiring discussions.

## References

  * [1] H. Murphy, “Hackers launch more than 1.2m attacks through log4j flaw,” _Financial Times_ , December 2021.
  * [2] T. Hunter and G. de Vynck, “The ’most serious’ security breach ever is unfolding right now. here’s what you need to know,” _Washington Post_ , December 2021.
  * [3] C. A. R. Hoare, “An axiomatic basis for computer programming,” _Communications of the ACM_ , vol. 12, no. 10, p. 576–580, oct 1969. [Online]. Available: https://doi.org/10.1145/363235.363259
  * [4] ——, “Programs are predicates,” in _Proc. of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages_. USA: Prentice-Hall, Inc., 1985, p. 141–155.
  * [5] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “Sel4: Formal verification of an os kernel,” in _Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles_ , ser. SOSP ’09. New York, NY, USA: Association for Computing Machinery, 2009, p. 207–220. [Online]. Available: https://doi.org/10.1145/1629575.1629596
  * [6] J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. Delignat-Lavaud, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Zanella-Béguelin, “Evercrypt: A fast, veriﬁed, cross-platform cryptographic provider,” in _IEEE Symposium on Security and Privacy_. IEEE, May 2020.
  * [7] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, “Hacl*: A verified modern cryptographic library,” in _Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security_ , ser. CCS ’17. New York, NY, USA: Association for Computing Machinery, 2017, p. 1789–1806. [Online]. Available: https://doi.org/10.1145/3133956.3134043
  * [8] N. Swamy, T. Ramananandro, A. Rastogi, I. Spiridonova, H. Ni, D. Malloy, J. Vazquez, M. Tang, O. Cardona, and A. Gupta, “Hardening attack surfaces with formally proven binary format parsers,” in _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ , ser. PLDI 2022. New York, NY, USA: Association for Computing Machinery, 2022, p. 31–45. [Online]. Available: https://doi.org/10.1145/3519939.3523708
  * [9] X. Leroy, “Formal verification of a realistic compiler,” _Communications of the ACM_ , vol. 52, no. 7, p. 107–115, jul 2009. [Online]. Available: https://doi.org/10.1145/1538788.1538814
  * [10] J. Kang, Y. Kim, C.-K. Hur, D. Dreyer, and V. Vafeiadis, “Lightweight verification of separate compilation,” _SIGPLAN Not._ , vol. 51, no. 1, p. 178–190, jan 2016. [Online]. Available: https://doi.org/10.1145/2914770.2837642
  * [11] T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein, “sel4: From general purpose to a proof of information flow enforcement,” in _2013 IEEE Symposium on Security and Privacy_ , 2013, pp. 415–429.
  * [12] P. Kocher, J. Horn, A. Fogh, D. Genkin, D. Gruss, W. Haas, M. Hamburg, M. Lipp, S. Mangard, T. Prescher, M. Schwarz, and Y. Yarom, “Spectre attacks: Exploiting speculative execution,” in _2019 IEEE Symposium on Security and Privacy (SP)_ , 2019, pp. 1–19.
  * [13] G. Heiser, G. Klein, and T. Murray, “Can we prove time protection?” in _Proceedings of the Workshop on Hot Topics in Operating Systems_ , ser. HotOS ’19. New York, NY, USA: Association for Computing Machinery, 2019, p. 23–29. [Online]. Available: https://doi.org/10.1145/3317550.3321431
  * [14] M. Y. Vardi, “Program verification: Vision and reality,” _Communications of the ACM_ , vol. 64, no. 7, p. 5, jun 2021. [Online]. Available: https://doi.org/10.1145/3469113
  * [15] L. Ren, “Analysis of nakamoto consensus,” Cryptology ePrint Archive, Paper 2019/943, 2019, https://eprint.iacr.org/2019/943. [Online]. Available: https://eprint.iacr.org/2019/943
  * [16] J. Neu, E. N. Tas, and D. Tse, “The availability-accountability dilemma and its resolution via accountability gadgets,” in _Financial Cryptography_ , ser. Lecture Notes in Computer Science, vol. 13411. Springer, 2022, pp. 541–559.
  * [17] ——, “Ebb-and-flow protocols: A resolution of the availability-finality dilemma,” in _IEEE Symposium on Security and Privacy_. IEEE, 2021, pp. 446–465.
  * [18] C. Herley and P. Van Oorschot, “Sok: Science, security and the elusive goal of security as a scientific pursuit,” in _Proceedings of the IEEE Symposium on Security and Privacy_ , ser. S&P 2017, 2017, pp. 99–120.
  * [19] K. R. Popper, _The Logic of Scientific Discovery_. London: Routledge, 1959.
  * [20] Y. Kim, R. Daly, J. Kim, C. Fallin, J. H. Lee, D. Lee, C. Wilkerson, K. Lai, and O. Mutlu, “Flipping bits in memory without accessing them: An experimental study of dram disturbance errors,” in _Proceeding of the 41st Annual International Symposium on Computer Architecture_ , ser. ISCA ’14. IEEE Press, 2014, p. 361–372.
  * [21] J. Noorman, J. V. Bulck, J. T. Mühlberg, F. Piessens, P. Maene, B. Preneel, I. Verbauwhede, J. Götzfried, T. Müller, and F. Freiling, “Sancus 2.0: A low-cost security architecture for iot devices,” _ACM Trans. Priv. Secur._ , vol. 20, no. 3, jul 2017. [Online]. Available: https://doi.org/10.1145/3079763
  * [22] I. D. O. Nunes, K. Eldefrawy, N. Rattanavipanon, M. Steiner, and G. Tsudik, “Vrased: A verified hardware/software co-design for remote attestation,” in _Proceedings of the 28th USENIX Conference on Security Symposium_ , ser. SEC’19. USA: USENIX Association, 2019, p. 1429–1446.
  * [23] M. Bognar, J. Van Bulck, and F. Piessens, “Mind the gap: Studying the insecurity of provably secure embedded trusted execution architectures,” in _2022 IEEE Symposium on Security and Privacy (SP)_ , 2022, pp. 1638–1655.
  * [24] S. Cauligi, C. Disselkoen, D. Moghimi, G. Barthe, and D. Stefan, “Sok: Practical foundations for software spectre defenses,” in _IEEE Symposium on Security and Privacy (S &P)_. IEEE, May 2022.
  * [25] M. Guarnieri, B. Köpf, J. Reineke, and P. Vila, “Hardware-software contracts for secure speculation,” in _IEEE Symposium on Security and Privacy_. IEEE, 2021, pp. 1868–1883.
  * [26] B. Greenman, S. Saarinen, T. Nelson, and S. Krishnamurthi, “Little tricky logic: Misconceptions in the understanding of ltl,” _The Art, Science, and Engineering of Programming_ , vol. 7, no. 7, pp. 1–37, 2023. [Online]. Available: https://doi.org/10.22152/programming-journal.org/2023/7/7
  * [27] T. Murray and P. van Oorschot, “Bp: Formal proofs, the fine print and side effects,” in _Proceedings of the IEEE Cybersecurity Development_ , ser. SecDev 2018, 2018, pp. 1–10.
  * [28] I. Lakatos, _Proofs and refutations_. Nelson London, 1963.
  * [29] N. Koblitz and A. Menezes, “Critical perspectives on provable security,” _Advances in Mathematics of Communications_ , vol. 13, no. 4, pp. 517–558, 2019. [Online]. Available: /article/id/5d2d9acd-8f7a-4e46-8e4a-dfab9701f215
  * [30] D. E. Denning, “The limits of formal security models,” https://faculty.nps.edu/dedennin/publications/National%20Computer%20Systems%20Security%20Award%20Speech.htm, 1999, accessed: 2023-03-09.
  * [31] S. Bratus, M. E. Locasto, M. L. Patterson, L. Sassaman, and A. Shubina, “Exploit programming: From buffer overflows to weird machines and theory of computation,” _USENIX ;login:_ , vol. 36, no. 6, Dec 2011.
  * [32] R. A. De Millo, R. J. Lipton, and A. J. Perlis, “Social processes and proofs of theorems and programs,” _Communications of the ACM_ , vol. 22, no. 5, p. 271–280, may 1979. [Online]. Available: https://doi.org/10.1145/359104.359106
  * [33] N. Mouha and C. Celi, “A vulnerability in implementations of sha-3, shake, eddsa, and other nist-approved algorithm,” Cryptology ePrint Archive, Paper 2023/331, 2023, https://eprint.iacr.org/2023/331. [Online]. Available: https://eprint.iacr.org/2023/331
  * [34] V. D’Silva, M. Payer, and D. Song, “The correctness-security gap in compiler optimization,” in _Proceedings of the IEEE Security and Privacy Workshops_ , ser. LangSec 2015, 2015, pp. 73–87.
  * [35] M. Böhme, “Tweet,” https://twitter.com/mboehme_/status/1630985423949365254, Feb 2023, accessed: 2022-03-12.
  * [36] T. Ormandy, “Zenbleed,” https://lock.cmpxchg8b.com/zenbleed.html, accessed: 2021-03-12.
  * [37] J. R. S. Vicarte, P. Shome, N. Nayak, C. Trippel, A. Morrison, D. Kohlbrenner, and C. W. Fletcher, “Opening pandora’s box: A systematic study of new ways microarchitecture can leak private data,” in _Proceedings of the 48th Annual International Symposium on Computer Architecture_ , ser. ISCA ’21. IEEE Press, 2021, p. 347–360. [Online]. Available: https://doi.org/10.1109/ISCA52012.2021.00035
  * [38] T. Dullien, “Security, moore’s law, and the anomaly of cheap complexity,” in _Proceedings of the International Conference on Cyber Conflict_ , ser. CyCon 2018, 2018.
  * [39] ——, “Weird machines, exploitability, and provable unexploitability,” _IEEE Transactions on Emerging Topics in Computing_ , vol. 8, no. 2, pp. 391–403, 2020.
  * [40] W.-P. De Roever, K. Engelhardt, J. Coenen, K.-H. Buth, P. Gardiner, Y. Lakhnech, and F. Stomp, _Data Refinement Model-Oriented Proof methods and their Comparison_. Cambridge University Press, 1998.
  * [41] J. Vanegue, “The weird machines in proof-carrying code,” in _Proceedings of the 2014 IEEE Security and Privacy Workshops_ , 2014, pp. 209–213.
  * [42] G. Balakrishnan and T. Reps, “Wysinwyx: What you see is not what you execute,” _ACM Trans. Program. Lang. Syst._ , vol. 32, no. 6, aug 2010. [Online]. Available: https://doi.org/10.1145/1749608.1749612
  * [43] W. Landi, “Undecidability of static analysis,” _ACM Lett. Program. Lang. Syst._ , vol. 1, no. 4, p. 323–337, dec 1992. [Online]. Available: https://doi.org/10.1145/161494.161501
  * [44] G. Ramalingam, “The undecidability of aliasing,” _ACM Trans. Program. Lang. Syst._ , vol. 16, no. 5, p. 1467–1471, sep 1994. [Online]. Available: https://doi.org/10.1145/186025.186041
  * [45] F. Cohen, “Computer viruses: Theory and experiments,” _Computers & Security_, vol. 6, no. 1, pp. 22–35, 1987.
  * [46] M. Böhme, “Statistical reasoning about programs,” in _Proceedings of the 44th International Conference on Software Engineering_ , ser. ICSE 2022, 2022\.
  * [47] K. Thompson, “Reflections on trusting trust,” _Commun. ACM_ , vol. 27, no. 8, p. 761–763, aug 1984. [Online]. Available: https://doi.org/10.1145/358198.358210
  * [48] C. Domas, “Breaking the x86 isa,” 2017, https://www.blackhat.com/docs/us-17/thursday/us-17-Domas-Breaking-The-x86-Instruction-Set-wp.pdf.
  * [49] ——, “God mode unlocked: Hardware backdoors in redacted x86,” 2018, https://www.youtube.com/watch?v=jmTwlEh8L7g&ab_channel=DEFCONConference.
  * [50] K. Lu and Q. Wu, “On the feasibility of stealthily introducing vulnerabilities in open-source software via hypocrite commits,” 2021.
  * [51] C. S. Calude and C. Müller, “Formal proof: Reconciling correctness and understanding,” in _Proceeding of the 16th Symposium Intelligent Computer Mathematics_ , ser. Lecture Notes in Computer Science, J. Carette, L. Dixon, C. S. Coen, and S. M. Watt, Eds., vol. 5625. Springer, 2009, pp. 217–232.
  * [52] M. N. Mansur, M. Christakis, V. Wüstholz, and F. Zhang, “Detecting critical bugs in smt solvers using blackbox mutational fuzzing,” in _Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ , ser. ESEC/FSE 2020. New York, NY, USA: Association for Computing Machinery, 2020, p. 701–712. [Online]. Available: https://doi.org/10.1145/3368089.3409763
  * [53] D. Winterer, C. Zhang, and Z. Su, “Validating smt solvers via semantic fusion,” in _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ , ser. PLDI 2020. New York, NY, USA: Association for Computing Machinery, 2020, p. 718–730. [Online]. Available: https://doi.org/10.1145/3385412.3385985
  * [54] S. Li and Z. Su, “Ubfuzz: Finding bugs in sanitizer implementations,” in _Proceedings of the ACM International Conference on Architectural Support for Programming Languages and Operating Systems_ , ser. ASPLOS ’24, 2024, p. 14.
  * [55] S. Bhat and H. Shacham, “Formal verification of the linux kernel ebpf verifier range analysis,” Technical Report, 2022, https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf. [Online]. Available: https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf
  * [56] S. Scannell, V. Palmiotti, and J. J. L. Jaimez, “Alice in kernel land: Lessons learned from the ebpf rabbit hole,” BlackHat Asia’23, 2023, https://i.blackhat.com/Asia-23/AS-23-Palmiotti-Alice-In-Kernel-Land-wp.pdf. [Online]. Available: https://i.blackhat.com/Asia-23/AS-23-Palmiotti-Alice-In-Kernel-Land-wp.pdf
  * [57] J. Jia, R. Sahu, A. Oswald, D. Williams, M. V. Le, and T. Xu, “Kernel extension verification is untenable,” in _Proceedings of the 19th Workshop on Hot Topics in Operating Systems_ , ser. HOTOS ’23. New York, NY, USA: Association for Computing Machinery, 2023, p. 150–157. [Online]. Available: https://doi.org/10.1145/3593856.3595892
  * [58] T. Dullien, “Keynote @ offensivecon: Why i love offensive work,” https://docs.google.com/presentation/d/1YcBqgccBcdn5-v80OX8NTYdu_-qRmrwfejlEx6eq-4E, 2020, accessed: 2023-03-09.
  * [59] N. Young and S. Krishnamurthi, “Early post-secondary student performance of adversarial thinking,” in _Proceedings of the 17th ACM Conference on International Computing Education Research_ , ser. ICER 2021. New York, NY, USA: Association for Computing Machinery, 2021, p. 213–224. [Online]. Available: https://doi.org/10.1145/3446871.3469743
  * [60] D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf, “Bugs as deviant behavior: A general approach to inferring errors in systems code,” in _Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles_ , ser. SOSP ’01. New York, NY, USA: Association for Computing Machinery, 2001, p. 57–72. [Online]. Available: https://doi.org/10.1145/502034.502041
  * [61] D. W. Woods, “Lemons and liability: Cyber warranties as an experiment in software regulation,” in _Blackhat_ , 2023.
  * [62] G. A. Akerlof, “The market for ”lemons”: Quality uncertainty and the market mechanism,” _The Quarterly Journal of Economics_ , vol. 84, no. 3, pp. 488–500, 1970.
  * [63] D. Rosenblum, “A practical approach to programming with assertions,” _IEEE Transactions on Software Engineering_ , vol. 21, no. 1, pp. 19–31, 1995\.
  * [64] H. Marco-Gisbert and I. Ripoll-Ripoll, “Exploiting linux and pax aslr’s weaknesses on 32- and 64-bit systems,” in _Blackhat Asia_ , 2016.
  * [65] C. Shannon, “Communication theory of secrecy systems,” _Bell System Technical Journal,_ , vol. 28, p. 656–715, Oktober 1949.
  * [66] D. Pavlovic, “Gaming security by obscurity,” in _Proceedings of the ACM New Security Paradigms Workshop_ , ser. NSPW. ACM, 2011, pp. 125–140.
  * [67] S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, “Oracle-guided component-based program synthesis,” in _Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering_ , ser. ICSE ’10. New York, NY, USA: Association for Computing Machinery, 2010, p. 215–224. [Online]. Available: https://doi.org/10.1145/1806799.1806833
  * [68] G. C. Necula, “Proof-carrying code,” in _Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ , ser. POPL ’97. New York, NY, USA: Association for Computing Machinery, 1997, p. 106–119. [Online]. Available: https://doi.org/10.1145/263699.263712
  * [69] M. Böhme, V.-T. Pham, and A. Roychoudhury, “Coverage-based greybox fuzzing as markov chain,” in _Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security_ , ser. CCS ’16. New York, NY, USA: Association for Computing Machinery, 2016, p. 1032–1043. [Online]. Available: https://doi.org/10.1145/2976749.2978428
  * [70] M. Leucker and C. Schallhart, “A brief account of runtime verification,” _The Journal of Logic and Algebraic Programming_ , vol. 78, no. 5, pp. 293–303, 2009, the 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS’07). [Online]. Available: https://www.sciencedirect.com/science/article/pii/S1567832608000775
  * [71] K. Claessen and J. Hughes, “Quickcheck: A lightweight tool for random testing of haskell programs,” _SIGPLAN Not._ , vol. 46, no. 4, p. 53–64, may 2011\. [Online]. Available: https://doi.org/10.1145/1988042.1988046
  * [72] Y. Zhang and A. Mesbah, “Assertions are strongly correlated with test suite effectiveness,” in _Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering_ , ser. ESEC/FSE 2015. New York, NY, USA: Association for Computing Machinery, 2015, p. 214–224. [Online]. Available: https://doi.org/10.1145/2786805.2786858
  * [73] K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov, “Addresssanitizer: A fast address sanity checker,” in _Proceedings of the 2012 USENIX Conference on Annual Technical Conference_ , ser. USENIX ATC’12. USA: USENIX Association, 2012, p. 28.
  * [74] G. Agha and K. Palmskog, “A survey of statistical model checking,” _ACM Trans. Model. Comput. Simul._ , vol. 28, no. 1, jan 2018. [Online]. Available: https://doi.org/10.1145/3158668
  * [75] E. T. Barr, M. Harman, P. McMinn, M. Shahbaz, and S. Yoo, “The oracle problem in software testing: A survey,” _IEEE Transactions on Software Engineering_ , vol. 41, no. 5, pp. 507–525, 2015.
  * [76] L. Kohnfelder and P. Garg, “The threats to our products,” _Microsoft Interface_ , April 1999.
  * [77] S. Roth, T. Barron, S. Calzavara, N. Nikiforakis, and B. Stock, “Complex security policy? a longitudinal analysis of deployed content security policies,” in _Proceedings of the 27th Network and Distributed System Security Symposium_ , ser. NDSS’20, 2020. [Online]. Available: https://par.nsf.gov/biblio/10173479
  * [78] P. T. Devanbu and S. Stubblebine, “Software engineering for security: A roadmap,” in _Proceedings of the Conference on The Future of Software Engineering_ , ser. ICSE ’00. New York, NY, USA: Association for Computing Machinery, 2000, p. 227–239. [Online]. Available: https://doi.org/10.1145/336512.336559
  * [79] J. P. Degabriele, K. Paterson, and G. Watson, “Provable security in the real world,” _Proceedings of the IEEE Security and Privacy_ , vol. 9, no. 3, pp. 33–41, 2011.
  * [80] J. V. Stoep, “Memory safe languages in android 13,” https://security.googleblog.com/2022/12/memory-safe-languages-in-android-13.html, Dec 2022, accessed: 2023-09-01.
  * [81] M. Abadi, M. Budiu, U. Erlingsson, and J. Ligatti, “Control-flow integrity principles, implementations, and applications,” _ACM Trans. Inf. Syst. Secur._ , vol. 13, no. 1, nov 2009. [Online]. Available: https://doi.org/10.1145/1609956.1609960
  * [82] H. Shacham, M. Page, B. Pfaff, E.-J. Goh, N. Modadugu, and D. Boneh, “On the effectiveness of address-space randomization,” in _Proceedings of the 11th ACM Conference on Computer and Communications Security_ , ser. CCS ’04. New York, NY, USA: Association for Computing Machinery, 2004, p. 298–307. [Online]. Available: https://doi.org/10.1145/1030083.1030124
  * [83] J. Ravichandran, W. T. Na, J. Lang, and M. Yan, “Pacman: Attacking arm pointer authentication with speculative execution,” in _Proceedings of the 49th Annual International Symposium on Computer Architecture_ , ser. ISCA ’22. New York, NY, USA: Association for Computing Machinery, 2022, p. 685–698. [Online]. Available: https://doi.org/10.1145/3470496.3527429
  * [84] A. Taylor, B. Nowierski, and K. Hara, “Use-after-freedom: MiraclePtr,” Sep. 2022\. [Online]. Available: https://security.googleblog.com/2022/09/use-after-freedom-miracleptr.html
  * [85] P. Kehrer, “Memory Unsafety in Apple’s Operating Systems,” Jul. 2019. [Online]. Available: https://langui.sh/2019/07/23/apple-memory-safety/
  * [86] “Queue hardening enhancements,” May 2019. [Online]. Available: https://security.googleblog.com/2019/05/queue-hardening-enhancements.html
  * [87] A. Gaynor, “Introduction to Memory Unsafety for VPs of Engineering,” Aug. 2019. [Online]. Available: https://alexgaynor.net/2019/aug/12/introduction-to-memory-unsafety-for-vps-of-engineering/
  * [88] R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer, “Rustbelt: Securing the foundations of the rust programming language,” _Proc. ACM Program. Lang._ , vol. 2, no. POPL, dec 2017. [Online]. Available: https://doi.org/10.1145/3158154
  * [89] D. Stenberg, “Tweet,” https://twitter.com/bagder/status/1360131939794042884, accessed: 2023-09-01.
  * [90] I. Goldberg, D. Wagner, R. Thomas, and E. A. Brewer, “A secure environment for untrusted helper applications confining the wily hacker,” in _Proceedings of the 6th Conference on USENIX Security Symposium, Focusing on Applications of Cryptography - Volume 6_ , ser. SSYM’96. USA: USENIX Association, 1996, p. 1.
  * [91] V. Costan and S. Devadas, “Intel sgx explained,” Cryptology ePrint Archive, Paper 2016/086, 2016, https://eprint.iacr.org/2016/086. [Online]. Available: https://eprint.iacr.org/2016/086
  * [92] Y. Juglaret, C. Hritcu, A. Amorim, B. Eng, and B. C. Pierce, “Beyond good and evil: Formalizing the security guarantees of compartmentalizing compilation,” in _2016 IEEE 29th Computer Security Foundations Symposium (CSF)_. Los Alamitos, CA, USA: IEEE Computer Society, jul 2016, pp. 45–60. [Online]. Available: https://doi.ieeecomputersociety.org/10.1109/CSF.2016.11
  * [93] J. Van Bulck, M. Minkin, O. Weisse, D. Genkin, B. Kasikci, F. Piessens, M. Silberstein, T. F. Wenisch, Y. Yarom, and R. Strackx, “Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution,” in _Proceedings of the 27th USENIX Security Symposium_. USENIX Association, August 2018, https://foreshadowattack.eu/.
  * [94] M. Brand, “Virtually unlimited memory: Escaping the chrome sandbox,” https://googleprojectzero.blogspot.com/2019/04/virtually-unlimited-memory-escaping.html, Apr. 2019, accessed: 2023-09-01.
  * [95] H. Lefeuvre, V. Badoiu, Y. Chen, F. Huici, N. Dautenhahn, and P. Olivier, “Assessing the impact of interface vulnerabilities in compartmentalized software,” in _NDSS_. The Internet Society, 2023.
  * [96] S. Fei, Z. Yan, W. Ding, and H. Xie, “Security vulnerabilities of sgx and countermeasures: A survey,” _ACM Comput. Surv._ , vol. 54, no. 6, jul 2021\. [Online]. Available: https://doi.org/10.1145/3456631
  * [97] A. Nilsson, P. N. Bideh, and J. Brorsson, “A survey of published attacks on intel SGX,” _CoRR_ , vol. abs/2006.13598, 2020.
  * [98] M. Dellago, D. Woods, and A. Simpson, “Characterising 0-day exploit brokers,” in _Proceedings of the 21st Workshop on the Economics of Information Security_ , ser. WEIS 2022, Jun. 2022.
  * [99] J. Saltzer and M. Schroeder, “The protection of information in computer systems,” _Proceedings of the IEEE_ , vol. 63, no. 9, pp. 1278–1308, 1975\.
  * [100] CoolStar and Tihmstar, “Jailbreaking ios in the postapocalyptic era,” NullCon Goa, 2022.
  * [101] S. Schechter, “How to buy better testing using competition to get the most security and robustness for your dollar,” in _Infrastructure Security_ , G. Davida, Y. Frankel, and O. Rees, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002, pp. 73–87.
  * [102] A. Musgrave and C. Pigden, “Imre Lakatos,” in _The Stanford Encyclopedia of Philosophy_ , Spring 2023 ed., E. N. Zalta and U. Nodelman, Eds. Metaphysics Research Lab, Stanford University, 2023.
  * [103] S. Mergendahl, N. Burow, and H. Okhravi, “Cross-language attacks,” in _NDSS_. The Internet Society, 2022\.
  * [104] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement,” in _Computer Aided Verification_ , E. A. Emerson and A. P. Sistla, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 154–169.
  * [105] X. Yang, Y. Chen, E. Eide, and J. Regehr, “Finding and understanding bugs in c compilers,” in _Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation_ , ser. PLDI ’11. New York, NY, USA: Association for Computing Machinery, 2011, p. 283–294. [Online]. Available: https://doi.org/10.1145/1993498.1993532
  * [106] H. Armstrong and M. Bishop, “Uncovering assumptions in information security,” in _Proceedings of the WISE4 Forth World Conference on Information Security Education_ , 2005.
  * [107] M. Chechik, “On safety, assurance, and reliability: a software engineering perspective (keynote),” in _ESEC/SIGSOFT FSE_. ACM, 2022, p. 2.
  * [108] B. Hawkes, “Exploit equivalence classes,” https://blog.isosceles.com/exploit-equivalence-classes/, Aug. 2023, accessed: 2023-09-01.
  * [109] I. Beer, “An analysis of an in-the-wild ios safari webcontent to gpu process exploit,” https://googleprojectzero.blogspot.com/2023/10/an-analysis-of-an-in-the-wild-ios-safari-sandbox-escape.html, Oct. 2023, accessed: 2023-10-13.