11institutetext: University of Waterloo and The Technion

# Verifying Verified Code††thanks: This research was supported by grants from
WHJIL and NSERC CRDPJ 543583-19.

Siddharth Priya 11 Xiang Zhou 11 Yusen Su 11 Yakir Vizel 22 Yuyan Bao 11 Arie
Gurfinkel 111122

###### Abstract

A recent case study from AWS by Chong et al. proposes an effective methodology
for Bounded Model Checking in industry. In this paper, we report on a followup
case study that explores the methodology from the perspective of three
research questions: (a) can proof artifacts be used across verification tools;
(b) are there bugs in verified code; and (c) can specifications be improved.
To study these questions, we port the verification tasks for aws-c-common
library to SeaHorn and KLEE. We show the benefits of using compiler semantics
and cross-checking specifications with different verification techniques, and
call for standardizing proof library extensions to increase specification
reuse. The verification tasks discussed are publicly available online.

##  1 Introduction

Bounded Model Checking (BMC) is an effective static analysis technique that
reduces program analysis to propositional satisfiability (SAT) or
Satisfiability Modulo Theories (SMT). It works directly on the source code. It
is very precise, e.g., accounting for semantics of the programming language,
memory models, and machine arithmetic. There is a vibrant ecosystem of tools
from academia (e.g., SMACK [24], CPAChecker [4], ESBMC [12]), industrial
research labs (e.g., Corral [19], F-SOFT [15]), and industry (e.g., CBMC [9],
Crux [13], QPR [5]). There is an annual software verification competition, SV-
COMP [3], with many participants. However, with a few exceptions, BMC is not
actively used in software industry. Especially, when compared to dynamic
analysis techniques such as fuzzing [25], or light-weight formal methods such
as static analysis [2].

Transitioning research tools into practice requires case-studies, methodology,
and best-practices to show how the tools are best applied. Until recently,
there was no publicly available industrial case study on successful
application of BMC for continuous verification111By _continuous verification_
, we mean verification that is integrated with continuous integration (CI) and
is checked during every commit. of C code. This has changed with [7] – a case
study from the Automated Reasoning Group (ARG) at Amazon Web Services (AWS) on
the use of CBMC for proving memory safety (and other properties) of several
AWS C libraries. This case study proposes a verification methodology with two
core principles: (a) verification tasks structured around units of
functionality (i.e., around a single function, as in a unit test), and (b) the
use of code to express specifications (i.e., pre-, post-conditions, and other
contextual assumptions). We refer to these as _unit proofs_ , and _Code as
Specification (CaS)_ , respectively. The methodology is efficient because
small verification tasks help alleviate scalability issues inherent in BMC.
More significantly, developers adopt, own, extend and even use specifications
(as code) in other contexts, e.g., unit tests. Admirably, AWS has released all
of the verification artifacts (code, specifications and verification
libraries)222https://github.com/awslabs/aws-c-
common/tree/main/verification/cbmc. Moreover, these are maintained and
integrated into Continuous Integration (CI). This gave us a unique opportunity
to study, validate, and refine the methodology of [7]. In this paper, we
report on our experience on adapting the verification tasks of [7] to two new
verification tools: a Bounded Model Checking engine of SeaHorn, and the
symbolic execution tool KLEE. We present our experience as a case study that
is organized around three Research Questions (RQ):

#### RQ1: Does CaS empower multiple tools for a common verification task?

Code is the _lingua franca_ among developers, compilers, and verification
tools. Thus, CaS makes specifications understandable by multiple verification
tools. To validate effectiveness of this hypothesis, we adapted the unit
proofs from AWS to different tools, and report on the experience in Sec. 3.1.
While giving a positive answer to RQ1, we highlight the importance of the
semantics used to interpret CaS, and that effectiveness of each tool depends
on specification styles.

#### RQ2: Are there bugs in verified code?

Specifications written by humans may have errors. Do such errors hide bugs in
verified implementations? What sanity checks are helpful to find bugs in
implementations _and_ specifications? The public availability of [7] is a
unique opportunity to study this question. In contrast to [7], we found no new
bugs in the library being verified (aws-c-common). However, we have found
multiple errors in specifications! Reporting them to AWS triggered a massive
review of existing unit proofs with many similar issues found and fixed. We
report the bugs, and techniques that helped us discover them, in Sec. 3.2.

#### RQ3: Can specifications be improved while maintaining CaS philosophy?

Some mistakes in specifications can be prevented by improvements to the
specification language. We propose a series of improvements that significantly
reduce specification burden. They are mostly in the form of built-in
functions, thus, familiar to developers. In particular, we show how to make
the verification of the linked_list data structure in aws-c-common
significantly more efficient, while making the proofs unbounded (i.e., correct
for linked list of any size).

In our case study, we used the BMC engine of SeaHorn [14] and symbolic
execution tool KLEE [6]. We have chosen SeaHorn because it is conceptually
similar to CBMC that was used in [7]. Thus, it was reasonable to assume that
all verification tasks can be ported to it. We are also intimately familiar
with SeaHorn. Thus, we did not only port verification tasks, but proposed
improvements to SeaHorn to facilitate the process. We have chosen KLEE because
it is a well-known representative of symbolic execution – an approach that is
the closest alternative to Bounded Model Checking.

Overall, we have ported all of the $169$ unit proofs of aws-c-common to
SeaHorn, and $153$ to KLEE. The case study represents a year of effort. The
time was divided between porting verification tasks, improving SeaHorn to
allow for a better comparison, and, many manual and semi-automated sanity
checks to increase confidence in specifications. Additionally, we have
experimented with using unit proofs as fuzz targets using LLVM fuzzing library
libFuzzer [25] and adapted $146$ of the unit proofs to libFuzzer.

We make all results of our work publicly available and reproducible at
https://github.com/seahorn/verify-c-common. In addition to what is reported in
this paper, we have developed an extensive CMake build system that simplifies
integration of additional tools. The case study is _live_ in the sense that it
is integrated in CI and is automatically re-run nightly. Thus, it is
synchronized both with the tools we use and the AWS library we verify.

We hope that our study inspires researchers to adapt their tools to industrial
code, and inspires industry to release verification efforts to study.

#### Caveats and non-goals.

We focus on the issues of methodology and sharing verification tasks between
different tools. The tools that we use have different strengths and
weaknesses. While they all validate user-supplied assertions, they check for
different built-in properties (e.g., numeric overflow, undefined behaviours,
memory safety). The goal is not to compare the tools head-to-head, or to find
the best tool for a given task. We have not attempted to account for the
differences between the tools. Nor have we tried to completely cover all
verification tasks by all tools. Our goal was to preserve the unit proofs of
[7] as much as possible to allow for a better comparison. For that reason,
while we do report on performance results for the different tools, we do not
describe them in detail. An interested reader is encouraged to look at the
detailed data we make available on GitHub. Furthermore, while we have applied
fuzzing to the unit proofs, we do not focus on effectiveness and applicability
of static vs dynamic verification but only on the issues of methodology.

To summarize, we make the following contributions: (a) we validate that CaS
can be used to share specifications between multiple tools, especially tools
that share the same techniques (i.e., BMC), or tools with related techniques
(i.e., BMC and Symbolic Execution); (b) we describe in details bugs that are
found in verified code (more specifically, in specifications), some are quite
surprising; (c) we suggest a direction to improve CaS with additional built-in
functions that simplify common specification; and (d) we make our system
publicly available allowing other researches to integrate their tools, use it
as a benchmark, and to validate new verification approaches on industrial
code.

The rest of the paper is structured as follows. Sec. 2 recalls the methodology
of unit proof and CaS. And Sec. 3 presents the architecture of the case study
and answers the three research questions. We discuss related work in Sec. 4
and offer concluding remarks in Sec. 5.

##  2 Unit Proofs with Code-as-Specification

In [7], a methodology for program verification is proposed that allows
developers to write specifications and proofs using the C programming
language. The core of the methodology are _unit proof_ 333In [7], these are
called _proof harnesses_. and _Code as Specification (CaS)_. A _unit proof_ is
similar to a _unit test_ in that it is a piece of a code (usually a method)
that invokes another piece of code (under test) and checks its correctness
[23]. Fig. 1 shows an example of a unit proof for the method
{aws_array_list_get_at_ptr}xspace,from aws-c-common library. It has three
parts: (1) the specification of {aws_array_list_get_at_ptr}xspace,i.e., pre-
(line 8) and post-conditions (lines 10–11); (2) a call to the function under
verification (line 9); and (3) the specification of the program context that
the method is called from (lines 2–7). Note that all specifications are
written directly in C. We call this specification style – CaS. Assumptions (or
pre-conditions) correspond to {__CPROVER_assume}xspace,and assertions (or
post-conditions) correspond to {assert}xspace.Specifications are factored into
functions. For example, {aws_array_list_is_valid}xspacespecifies a
representation invariant of the array list. In this unit proof, the context is
restricted to a list of bounded size but with unconstrained elements and an
{index}xspace with(intentionally) unspecified value of type
{size_t}xspace.Even without expanding the code further, its meaning is clear
to any C developer familiar with the library.

The unit proof is verified with CBMC [9]. CBMC uses a custom SMT solver to
check that there are no executions that satisfy the pre-conditions and violate
at least one of the assertions (i.e., a counterexample). Together with the
explicit assertions, CBMC checks built-in properties: memory safety and
integer overflow.

⬇ 1void aws_array_list_get_at_ptr_harness() { 2 struct aws_array_list list; 3
/* memhavoc(&list, sizeof(struct aws_array_list))); */ 4
__CPROVER_assume(aws_array_list_is_bounded(&list)); 5
ensure_array_list_has_allocated_data_member(&list); 6 void **val =
can_fail_malloc(sizeof(void *)); 7 size_t index /* = nd_size_t() */; 8
__CPROVER_assume(aws_array_list_is_valid(&list) && val != NULL); 9 if
(aws_array_list_get_at_ptr(&list, val, index) == AWS_OP_SUCCESS) 10
assert(list.data != NULL && index < list.length); 11
assert(aws_array_list_is_valid(&list)); }

Figure 1: The unit proof of aws_array_list_get_at_ptr from [7].

According to [7], CaS and unit proofs are a practical and productive
verification methodology. It has been used successfully to verify memory
safety (and other properties) of multiple AWS projects, including the aws-c-
common library that we use in our case study. The library provides cross
platform configuration, data structures, and error handling support to a range
of other AWS C libraries and SDKs. It is the foundation of many security
related libraries, such as the AWS Encryption SDK for C [7]. It contains $13$
data structures, $169$ unit proofs that verify over $20$K lines of code (LOC).
Fig. 2 shows the LOC and running time for each data structure.

|  | LOC |  |  CBMC (s) |  |  SeaHorn (s) |  |  KLEE (s)
---|---|---|---|---|---|---|---|---
category |  num |  avg |  min |  max |  |  avg |  std |  |  avg |  std |  |  count |  avg | std
arithmetic |  6 |  33 |  11 |  40 |  |  3.8 |  0.8 |  |  0.6 |  0.1 |  |  6 |  0.9 | 0.3
array |  4 |  97 |  78 |  112 |  |  5.6 |  0.0 |  |  1.7 |  0.7 |  |  4 |  32.3 | 6.0
array_list |  23 |  126 |  77 |  181 |  |  35.8 |  60.8 |  |  2.5 |  3.3 |  |  23 |  55.4 | 49.3
byte_buf |  29 |  97 |  50 |  188 |  |  17.6 |  47.3 |  |  1.0 |  0.8 |  |  27 |  75.3 | 124.1
byte_cursor |  24 |  98 |  47 |  179 |  |  6.9 |  3.8 |  |  1.0 |  0.5 |  |  17 |  12.8 | 14.4
hash_callback |  3 |  115 |  49 |  198 |  |  9.7 |  5.5 |  |  4.9 |  3.6 |  |  3 |  64.0 | 45.5
hash_iter |  4 |  177 |  169 |  185 |  |  12.8 |  9.2 |  |  9.2 |  15.0 |  |  3 |  20.8 | 9.7
hash_table |  19 |  172 |  36 |  328 |  |  23.5 |  33.3 |  |  5.3 |  7.5 |  |  15 |  104.6 | 333.4
linked_list |  18 |  115 |  17 |  219 |  |  58.9 |  209.4 |  |  2.0 |  2.1 |  |  18 |  0.7 | 0.1
others |  2 |  15 |  10 |  21 |  |  3.5 |  0.0 |  |  0.5 |  0.0 |  |  1 |  0.7 | –
priority_queue |  15 |  187 |  136 |  258 |  |  208.1 |  303.4 |  |  10.6 |  16.9 |  |  15 |  46.4 | 11.6
ring_buffer |  6 |  155 |  56 |  227 |  |  20.0 |  19.5 |  |  29.5 |  34.2 |  |  6 |  48.1 | 26.4
string |  15 |  87 |  11 |  209 |  |  6.3 |  1.3 |  |  2.9 |  1.8 |  |  15 |  139.7 | 159.7
Total |  168 |  Loc |  20,190 |  |  |  Time |  6,475 |  |  Time |  691 |  |  Time |  8,577 |

Figure 2: Verification results for CBMC, SeaHorn and KLEE.

##  3 Case Study

Figure 3: Architecture of the case study.

The architecture of our case study is shown in Fig. 3. To compare with CBMC,
we use two tools based on the LLVM framework [20]: SeaHorn and KLEE. SeaHorn
[14] is a verification framework. We used the bit- and memory-precise BMC
developed during the case study. Its techniques are closest to CBMC. KLEE [6]
is a well-known symbolic execution tool. It is an alternative to BMC for
bounded exhaustive verification. In addition, we have experimented with
libFuzzer – a coverage-guided random testing framework. It does no symbolic
reasoning, and, together with address sanitizer, is known to be effective at
discovering memory errors. Fuzzing results are available online.
444https://seahorn.github.io/verify-c-common/fuzzing_coverage/index.html.

The rest of the section describes the research questions and our findings.

###  3.1 RQ1: Does CaS Empower Multiple Tools?

Hypothetically, CaS methodology enables sharing the same formal specification
among multiple, potentially distinct, tools and techniques. For example,
semantic analyses of IDEs and compilers can catch simple semantics bugs and
inconsistencies in specifications. Fuzzers can validate specifications through
testing. Symbolic execution can supplement BMC by capitalizing on a different
balance in performance versus precision. Static analysis tools can be used to
compute inductive invariants. However, is the hypothesis true in practice?

To validate the hypothesis, we adapted the unit proofs from aws-c-common to
two distinct verification techniques: BMC with SeaHorn and symbolic execution
with KLEE. We have also attempted to use unit proofs as fuzz targets for
libFuzzer. While our experience supports the hypothesis, we encountered two
major challenges: _semantics_ and _effectiveness of specifications_.

#### Semantics.

Code without semantics is meaningless. Developers understand code without
being versed in formal semantics, however, many technical details and “corner
cases” are often debated. This is especially true for C – _“the semantics of C
has been a vexed question for much of the last 40 years”_ [21]. Clear
semantics are crucial when code (and CaS) are used with multiple tools.

The unit proofs in [7] do not follow the C semantics. For example, consider
the proof in Fig. 1. According to C, it has no meaning as both
{list}xspace(line 2) and {index}xspace (line~7)are used uninitialized. CBMC
treats uninitialized variables as non-deterministic. So it is well-defined for
CBMC, but not for other tools.

What is a good choice of semantics for CaS? In [21], two semantics are
described – the ISO C Standard and the _de facto_ semantics of compilers.
Developers understand (and use) the de facto semantics. For example,
comparison of arbitrary pointers is undefined according to ISO C, but defined
consistently in mainstream compilers (and used in aws-c-common!). Therefore,
we argue that CaS must use the de facto semantics. Furthermore, unit proofs
must be compilable and, therefore, executable, so developers can execute them
not _just_ in their heads (like with [7]). Note that de facto semantics is not
complete with regards to C semantics, but is a commonly agreed upon subset.
What de facto semantics does not cover is compiler dependent semantics.

In our experience, using CaS with the de facto semantics is not hard. For
example, to adapt Fig. 1, we introduced {memhavoc}xspaceand
{nd_size_t}xspace,shown as comments, that fills a memory region at a given
address with non-deterministic bytes, and returns a non-deterministic value of
type {size_t}xspace,respectively.

#### Effectiveness of specifications.

We used three different tools on the same unit proof. Each tool requires
slightly different styles of specifications to be effective. We believe that
these stylistic differences between specifications can be captured by
traditional code refactoring techniques (i.e., functions, macros, etc.).
However, this is not easy whenever the specifications have not been written
with multiple tools (and with their strengths and weaknesses) in mind. A
significant part of our work has been in refactoring unit proofs from [7] to
be more modular.

We illustrate this with the pre-condition for the {byte_buf}xspacedata-
structure. In [7], data structures are assumed to be initially non-
deterministic, and various assumptions throughout the unit proof are used to
restrict it (e.g., lines 2–5 in Fig. 1). This impedes specification re-use
since different tools work well with different styles of pre-conditions. For
example, symbolic execution and fuzzing require memory to be explicitly
allocated, and all tools that use de-facto semantics require all memory be
initialized before use.

For {byte_buf}xspace,we factored out its pre-conditions into a function
{init_byte_buf}xspace.\footnote{Similarly,we introduced
{init_array_list}xspaceto replace lines 2–5 in Fig. 1. Its implementations for
SeaHorn, KLEE, and libFuzzer are shown in LABEL:fig:init-impls. It takes
{buf}xspacestructure as input, and initializes its fields to be consistent
with the representation invariant of {byte_buf}xspace.
\newsavebox{\figseainitlstbox}
\begin{lrbox}{\figseainitlstbox}\begin{lstlisting}[escapechar=@] size_t len =
nd_size_t(); size_t cap = nd_size_t(); assume(len ¡= cap); assume(cap ¡=
MAX_BUFFER); buf-¿len = len; buf-¿capacity = cap; buf-¿buffer =
can_fail_malloc( cap * sizeof(*(buf-¿buffer))); buf-¿allocator =
sea_allocator(); @ @

(a) for SeaHorn

⬇ size_t cap = nd_size_t(); assume(cap <= MAX_BUFFER); buf->buffer =
can_fail_malloc( cap * sizeof(*(buf->buffer))); if (buf->buffer) { size_t len
= nd_size_t(); assume(len <= cap); buf->len = len; buf->capacity = cap; } else
{ buf->len = 0; buf->capacity = 0; } buf->allocator = sea_allocator();

(b) for KLEE

⬇ size_t len = nd_size_t(); size_t cap = nd_size_t(); cap len = (cap == 0) ? 0
: len buf->len = len; buf->capacity = cap; buf->buffer = can_fail_malloc( cap
* sizeof(*(buf->buffer))); buf->allocator = sea_allocator();

(c) for libFuzzer

Figure 4: Tool-specific implementations for
{{{initialize_byte_buf}xspace.label{fig:init-impls}}}

SeaHorn initialization is closest to the original of [7]. Fields are
initialized via calls to external functions ({nd_<type>}xspace)that are
assumed to return arbitrary values. Representation invariants (i.e., length is
less or equal to capacity), as well as any upper bounds on buffer size are
specified with _assumptions_. Note that {can_fail_malloc}xspaceinternally
initializes allocated memory via a call to {memhavoc}xspace,ensuring that
reading {buf->buffer}xspaceis well-defined. KLEE initialization is similar to
SeaHorn, but special care must be taken about the placement of assumptions,
and implementation of {can_fail_malloc}xspace.In particular, KLEE prefers that
memory allocation functions are given explicit size, otherwise, it picks a
concrete size non-deterministically. Special cases, like
{buf->buffer}xspacebeing {NULL}xspace,are split in the initialization to aid
KLEE during symbolic execution. Similar changes can be done for SeaHorn, but
are not as effective. For that reason, we chose to keep SeaHorn initialization
as close to [7] as possible, but adjusted the one for KLEE to be most
effective. libFuzzer initialization is the most different since non-
determinisim must be replaced by randomness. In this case, {nd_<type>}xspace
functionsare implemented using the random inputs generated by libFuzzer.
_Assumptions_ are implemented by aborting the current fuzzing run if the
condition evaluates to {false}xspace.Of course, this limits fuzzing
effectiveness since the fuzzer must randomly guess inputs to pass all of the
assumptions. For that reason, as many assumptions as possible are modeled by
an explicit initialization. For example, in line 3 of 4(c), {cap}xspaceis re-
assigned to the modulo of {MAX_BUFFER}xspaceif libFuzzer generated a value
exceeding {MAX_BUFFER}xspace.This way, code after line 3 always executes
regardless of the return value of {nd_size_t()}xspacein line 4(c). Overall,
our results indicate that CaS empowers multiple verification tools to share
specifications among them. Common refactoring techniques make specifications
sharing effective. Specifications are easiest to share among tools that use
similar techniques.

#### Discussion.

We conclude this section with a discussion of our experience in using de facto
semantics. First, the code of aws-c-common is written with de facto semantics
in mind. We found that in [7] it had to be extended with many conditional
compilation flags to provide alternative implementations that are compatible
with CBMC or that instruct CBMC to ignore some seemingly undefined behavior.
However, we have not changed any lines of aws-c-common. We analyze the code
exactly how it is given to the compiler – improving coverage. Second, a
compiler may generate different target code for different architectures. By
using the compiler as front-end, we check that the code is correct as compiled
on different platforms. This is another advantage of CaS. Third, compilers may
provide additional safety checks. For example, aws-c-common uses GCC/Clang
built-in functions for overflow-aware arithmetic. By using de facto semantics,
all the tools used in the case study were able to deal with this in both CaS
and code seamlessly. Fourth, aws-c-common uses inline assembly to deal with
speculative execution-based vulnerabilities [17]. While inline assembly is not
part of the ISO C standard, it is supported by compilers. Thus, it is not a
problem for libFuzzer. We developed techniques to handle inline asm in
SeaHorn. For KLEE, we had to ignore such unit proofs.

###  3.2 Are there bugs in verified code?

Specifications may have errors as they are just programs: “Writing
specifications can be as error-prone as writing programs”.[22] Although [7]
suggests to use code coverage and code review to increase the confidence in
specifications, we still found non-trivial bugs. We summarize three most
interesting ones below. A complete list of all bugs we found is available in
App. 0.A.

⬇ 1typedef 2struct byte_buf { 3 char* buf; 4 int len, cap; 5} BB; 6bool
BB_is_ok(BB *b) 7{ return (b->len == 0 8 || b->buf); } (d) bug 1

⬇ 1 assume(0 <= b && b <= 10); 2 if (a < (b - 5) && 3 a >= (b + 5)) 4 { 5
assert(c > 0); 6 } 7 8 9 (e) bug 2

⬇ 1void ht_del_over(HASH_TB *t) { 2 /* remove entry */ 3 /* t->entry_count--;
*/ 4} 5 6 7 8 (f) bug 3

Figure 5: Simplified code for specification bugs.

#### Bug 1.

4(d) shows the definition of {byte}buffer that is a length delimited byte
string. Its data representation should be either the buffer ({buf}xspace)is
{NULL}xspaceor its capacity ({cap}xspace)is 0 (not the {len}xspaceas defined
in {BB_is_ok}xspace). Wefound this bug by a combination of sanity checks in
SeaHorn and our model of the memory allocator (i.e., {malloc}xspace).More
details are explained in 0.A.1.The bug did not manifest in [7] because other
pre-conditions ensured that {buf}xspaceis always allocated. Our report of this
bug to AWS triggered a massive code auditing effort in aws-c-common and
related libraries where many related issues were found.555An example is
https://github.com/awslabs/aws-c-common/pull/686/commits.

#### Bug 2.

4(e) shows a verification pattern where a property (line 5) is checked on the
program path (from lines 1 to 5). As the condition at lines 2 and 3 can never
be true, the property cannot be checked either. Our vacuity detection
(discussed later) found the bugs occurring in this pattern. More details on
the bug can be found in 0.A.4. Note that the bug was missed by the code
coverage detection used by CBMC, thus, may have been present for several
years.

#### Bug 3.

To make verification scalable, the verification of method A that calls another
method B may use a _specification stub_ that approximates the functionality of
B. AWS adopts this methodology when verifying the iterator of a hash table.
The iterator calls a function {ht_del}xspaceto remove an element in a hash
table. During verification {ht_del}xspaceis approximated by a specification
stub shown in 4(f). However, the approximation does not decrement
{entry_count}xspace,i.e., line 3 should be added to the spec for correct
behavior. In [7], the use of the buggy stub hides an error in the
specification. See more details in 0.A.6.

#### Discussion.

Code coverage of a unit proof is, at best, a sanity check for CaS. It reports
which source lines of the specification and code under verification are
covered under execution. However, because source lines can remain uncovered
for legitimate reasons e.g., dead code, interpreting a coverage report is not
straightforward. There is no obvious _pass/fail_ criterion. Thus, we found
that code coverage may be insufficient to detect bugs in CaS reliably. In
fact, bugs exist for multiple years even after code coverage failures. To help
find bugs in CaS with SeaHorn, we adapted _vacuity detection_ [18] to detect
unreachable post-conditions. Vacuity detection checks that every assert
statement is reachable. We encountered engineering challenges when developing
vacuity detection. For example, we received spurious warnings due to code
duplication. We silenced such warnings by only reporting a warning if all
duplicate asserts reported a vacuity failure. In addition, due to CaS, an
unreachable assertions may be removed by compiler’s dead code elimination.
This is not desirable for vacuity detection. To mitigate this issue, we report
when dead code is eliminated. However, since many eliminations are unrelated
to specs, there is noise in the report which makes it un-actionable.
Interaction between dead code removal by the compiler and vacuity detection
remains an open challenge for us. We have found bugs in specifications, but we
do not know what bugs remain. As shown in this section, the bugs were found
with a combination of manual auditing and tools. However, these techniques are
far from complete.

###  3.3 Can specifications be improved while maintaining the CaS philosophy?

⬇ 1linked_list l; 2Node *p = malloc(sizeof(Node)); 3l.head.next = p; 4for (int
idx=0; idx < MAX; idx++) { 5 Node *n = malloc(sizeof(Node)); 6 p->next = n; 7
p = n; } 8p->next = &l.tail; 9l.tail.prev = p; 10list_front(l); 11Node *nnode
= l.head.next; 12for (int idx=0; idx < MAX; idx++) { 13 nnode = nnode->next; }
14assert(nnode == l.tail); (a) Spec in the style of [7]

⬇ 1linked_list l; 2Node *n = malloc(sizeof(Node)); 3n->next = nd_voidp();
4l.head.next = n; 5l.tail.prev = nd_voidp(); 6list_front(l);
7assert(l.head.next == n); (b) New specification

Figure 6: Simplified code for differing CaS specifications.

⬇ 1 char buf[SZ]; 2 init_buf(buf, SZ); 3 int idx = nd_int(); 4 assume(0 <= idx
&& idx < SZ); 5 char saved = buf[idx]; 6 read_only_op(buf); 7 assert(saved ==
buf[idx]); (a) Spec in style of [7]

⬇ 1 char buf[SZ]; 2 init_buf(buf, SZ); 3 tracking_on(); 4 read_only_op(buf); 5
assert(!is_mod(buf)); (b) Spec using a built-in {is_mod}xspace

Figure 7: Two styles of specifications for a read only buffer operation. There
are many alternative ways to express a specification in CaS. In this section,
we illustrate how to make proofs more efficient and make specs more readable.
For example, a unit proof can fully instantiate a data structure (as in a unit
test), or minimally constrain it (as in [7]). In this section, we illustrate
this by describing our experience in making {linked_list}xspaceunit proofs
unbounded (and more efficient). Furthermore, we believe that extending the
specification language with additional verifier-supported built-in functions
simplifies specs while making them easier to verify. We illustrate this with
the built-ins developed for SeaHorn to specify absence of side-effects.

#### Linked List.

A common pattern in _unit proofs_ is to assume the representation invariant of
a data structure, and to assert it after invocation of the function under
verification along with other properties that must be maintained by the
function. For example, a simplified version of its unit proof from [7] is
shown in 5(a). The pre-conditions are specified by (explicitly) creating a
list in lines 4–7 using a loop. The post-condition is checked by completely
traversing the list in lines 12–14. This specification is simple since it
closely follows the style of unit tests. However, it is inefficient for BMC:
(a) unrolling the loops in the pre- and post-conditions blows up the symbolic
search space; (b) it makes verification of the loop-free function
{list_front}xspacebounded, i.e., verification appears to depend on the size of
the list in the pre-conditions. Our alternative formulation is to construct a
partially defined linked list stub as shown in 8a. This stub can be used to
verify {list_front}xspacesince it is expected that only the first node after
head is accessed. The resulting CaS is shown in 5(b). The {next}xspacefield of
{n}xspacepoints to a potentially invalid address (returned by
{nd_voidp}xspace).Either {list_front}xspacenever touches {n->next}xspaceor has
a memory fault. Finally, the assert on line 7 in 5(b) checks that
{list_front}xspacedid not modify the head of the list either. If there is no
memory fault, then {list_front}xspacedid not modify the linked list after the
node {n}xspace.Our specification is not inductive. It uses the insight that
the given linked list API only ever accesses a single element. It, therefore,
avoids loops in both the pre- and post-conditions and verifies
{list_front}xspacefor linked lists of any size. Unfortunately, our new spec in
5(b) is difficult to understand by non-experts because it relies on the
interplay between {nd_voidp}xspaceand memory safety checking. To make the spec
accessible, we hide the details behind a helper API.
LABEL:fig:linked_list_front_after shows the unit proof for
{aws_linked_list_front}xspacewith this API. The function
{sea_nd_init_aws_linked_list_from_head}xspaceconstructs partial
{aws_linked_list}xspace instanceswith non-deterministic length (as shown in
8a). The function {aws_linked_list_save_to_tail}xspace savesconcrete linked
list nodes from the partial {aws_linked_list}xspace.Finally, the function
{is_aws_list_unchanged_to_tail}xspace isused in post-conditions to check that
linked list nodes are not modified. The unit proof for
{aws_linked_list_front}xspaceis not only more efficient than the original CBMC
proof, but it is also a _stronger_ specification. For example, if
{aws_linked_list_front}xspace removesor modifies a linked list node, our unit
proof catches this as a violation, while the original proof only checks
whether the returned value is valid and whether the linked list is well
formed. The API we devised is generalized to work with all linked list
operations in {aws-c-common}xspace.For operations which access the node before
the tail we construct a partially defined stub as shown in 8b while 8c is
constructed for operations which access the list from both ends. We provide
corresponding versions of the above API to save and check immutability of
linked list nodes for each kind of stub. Figure 8: Linked list stubs for
proofs.

⬇ 1 void aws_linked_list_front_harness() { 2 /* data structure */ 3 struct
aws_linked_list list; 4 struct saved_aws_linked_list to_save = {0}; 5 size_t
size; 6 7 sea_nd_init_aws_linked_list_from_head(&list, &size); 8 struct
aws_linked_list_node *start = &list.head; 9
aws_linked_list_save_to_tail(&list, size, start, &to_save); 10 11 //
precondition in function does not accept empty linked list 12
assume(!aws_linked_list_empty(&list)); 13 14 /* perform operation under
verification */ 15 struct aws_linked_list_node *front =
aws_linked_list_front(&list); 16 17 /* assertions */ 18 sassert(list.head.next
== front); 19 sassert(aws_linked_list_node_prev_is_valid(front)); 20
sassert(aws_linked_list_node_next_is_valid(front)); 21
sassert(is_aws_list_unchanged_to_tail(&list, &to_save)); 22 23 return 0; 24 }

Figure 9: SeaHorn unit proof for
{{{aws_linked_list_front}xspace.label{fig:linked_list_front_after}}}

#### Increasing CaS expressiveness.

Verification tools should provide built-ins to aid in concise specifications.
Moreover, such built-ins enable specifications that are not otherwise
expressible in CaS. For example, 6(b) uses a SeaHorn built-in,
{is_mod}xspace,to specify that {read_only_op}xspacedoes not change the buffer.
This built-in returns true if memory pointed by its argument is modified since
the last call to {tracking_on}xspace. Incontrast, the original specification
for CBMC in 6(a) is tricky. It saves a byte from some position in the buffer
(lines 3–5), and checks that it is not changed (line 7). This example
illustrates that built-ins make specifications simpler and more direct. They
ease specification writing for users and might be exploited efficiently by
verification tools. As another example, SeaHorn provides a built-in
{is_deref}xspaceto check that a memory access is within bounds, which is not
(easily) expressible in C.

#### Discussion.

CaS enables concise specifications and efficient proofs. As advanced
verification techniques may not generalize, a standard extension is needed,
such as verification-specific built-in functions. The semantics of these can
be provided by a run-time library, validated by fuzzing and supported by
multiple verification tools. Additional case studies are needed to identify a
good set of built-ins. A standard extension can increase specification reuse
and make verification more productive and effective.

##  4 Related work

To our knowledge, [7] is the first significant, publicly available, example of
an application of BMC on industrial code that is actively maintained with the
code. Thus, our work is the first exploration of potential issues with
software verified in this way. The closest verification case studies are
coreutils with KLEE [6] and busybox ls with CBMC [16]. However, those focus on
the scalability of a specific verification technology, while we focus on
methodology, reuse, and what bugs might be hidden in the verification effort.
As we mentioned in the introduction, the Software Verification Competition
(SV-COMP) [3] provides a large collection of benchmarks, and, an annual
evaluation of many verification tools. However, it is focused on performance
and soundness of the tools. The benchmarks are pre-processed to fit the
competition format. At that stage, it is impossible to identify and evaluate
the specifications, or to modify the benchmarks to increase efficiency of any
particular tool. We hope that our case study can serve as an alternative
benchmark to evaluate suitability of verification tools for industrial
transition. In addition to [7], there has been number of other recent
applications of BMC at AWS, including [11, 8, 10]. However, they are either
not publicly available, too specialized, or not as extensive as the case study
in [7]. Using code as specification has a long history in verification tools,
one prominent example is Code Contracts introduced in Spec♯ [1]. One important
difference is that in our case CaS is used to share specifications between
completely different tools that only share the semantics of the underlying
programming language, and the language itself is used to adapt specifications
to the tools.

##  5 Conclusion

This case study would not have been possible without artifacts released by AWS
in [7]. To our knowledge, it is the first publicly available application of
BMC (to software) in industry. Related case studies on verification are those
on coreutils with KLEE [6] and on busybox ls with CBMC [16]. SV-COMP is a
large repository of benchmarks, but its goals are different from an actively
maintained industrial project. The availability of both methodology and
artifacts has given us a unique opportunity to study how verification is
applied in industry and to improve verification methodology. We encourage
industry to release more benchmarks to enable further studies by the research
community. In addition to answering the research questions, we are
contributing a complete working system that might be of interest to other
researchers. We have implemented a custom build system using CMake that
simplifies integrating new tools. We provide Docker containers to reproduce
all of the results. We created continuous integration (CI) on GitHub that
nightly re-runs all the tools on the current version of aws-c-common. Since we
use standard tools, the project integrates seamlessly into IDEs and
refactoring tools. The CI runs are done in parallel by CTest. Running SeaHorn
takes under $8$ minutes! While comparing different tools on performance is not
our primary concern, in Fig. 2, we show the running time for all of the
verification tools, collected on the same machine. Runtime for individual unit
proofs are shown in App. 0.B (and online). For libFuzzer, we make the detailed
coverage report available online. We stress that while the tools check the
same explicit assertions, they check different built-in properties. Thus,
running time comparison must be taken with a grain of salt. Our main
conclusion is in agreement with [7], and we strengthen the evidence for it.
CaS is a practical and scalable approach for specifications that is easy to
understand and empowers many tools. We argue that using de facto compiler
semantics in CaS is key for enabling many verification tools, each with its
own characteristic, to be used on the same verification problem. We find that
specifications can be written in different ways and specification writer must
account for both verification efficiency and developer readability. We suggest
that a set of common built-ins be shared by different verification tools. Such
built-ins improve the expressive power of CaS while retaining portability
across verification tools. With built-ins defined in a specification library,
software developers will be able to write unit proofs in a way no difference
than programming with libraries provided by some framework. Today, formal
verification is not the primary means of building confidence in software
quality. Our hope is that case studies like this one are useful to both
software engineering researchers and practitioners who want to make formal
methods an integral part of software development. To further this agenda, we
plan to continue applying the CaS methodology to larger and more complex code
bases (and languages) in the future.

## References

  * [1] Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81–91 (2011)

* [2] Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Gros, C., Kamsky, A., McPeak, S., Engler, D.R.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010), https://OPTdoi.org/10.1145/1646353.1646374
* [3] Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 347–367. Springer (2020)
* [4] Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6806, pp. 184–190. Springer (2011)
* [5] Büning, M.K., Sinz, C., Faragó, D.: QPR verify: A static analysis tool for embedded software based on bounded model checking. In: Software Verification - 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20-21, 2020, Revised Selected Papers. Lecture Notes in Computer Science, vol. 12549, pp. 21–32. Springer (2020)
* [6] Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. pp. 209–224. USENIX Association (2008)
* [7] Chong, N., Cook, B., Kallas, K., Khazem, K., Monteiro, F.R., Schwartz-Narbonne, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Code-level model checking in the software development workflow. In: ICSE-SEIP 2020: 42nd International Conference on Software Engineering, Software Engineering in Practice, Seoul, South Korea, 27 June - 19 July, 2020\. pp. 11–20. ACM (2020)
* [8] Chudnov, A., Collins, N., Cook, B., Dodds, J., Huffman, B., MacCárthaigh, C., Magill, S., Mertens, E., Mullen, E., Tasiran, S., Tomb, A., Westbrook, E.: Continuous formal verification of amazon s2n. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10982, pp. 430–446. Springer (2018)
* [9] Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2988, pp. 168–176. Springer (2004)
* [10] Cook, B., Döbel, B., Kroening, D., Manthey, N., Pohlack, M., Polgreen, E., Tautschnig, M., Wieczorkiewicz, P.: Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. pp. 185–193. IEEE (2020), https://OPTdoi.org/10.34727/2020/isbn.978-3-85448-042-6_26
* [11] Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10982, pp. 467–486. Springer (2018), https://OPTdoi.org/10.1007/978-3-319-96142-2_28
* [12] Gadelha, M.Y.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018. pp. 888–891. ACM (2018)
* [13] Galois: Crux: A Tool for Improving the Assurance of Software Using Symbolic Testing, https://crux.galois.com/
* [14] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn Verification Framework. In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp. 343–361. Springer (2015)
* [15] Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-soft: Software verification platform. In: Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3576, pp. 301–306. Springer (2005)
* [16] Kim, Y., Kim, M.: SAT-Based Bounded Software Model Checking for Embedded Software: A Case Study. In: 21st Asia-Pacific Software Engineering Conference, APSEC 2014, Jeju, South Korea, December 1-4, 2014. Volume 1: Research Papers. pp. 55–62. IEEE Computer Society (2014)
* [17] Kocher, P., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: Exploiting speculative execution. meltdownattack.com (2018)
* [18] Kupferman, O.: Sanity checks in formal verification. In: CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4137, pp. 37–51. Springer (2006)
* [19] Lal, A., Qadeer, S.: Powering the static driver verifier using Corral. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 \- 22, 2014. pp. 202–212. ACM (2014)
* [20] Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA. pp. 75–88. IEEE Computer Society (2004)
* [21] Memarian, K., Matthiesen, J., Lingard, J., Nienhuis, K., Chisnall, D., Watson, R.N.M., Sewell, P.: Into the depths of C: elaborating the de facto standards. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. pp. 1–15. ACM (2016)
* [22] Moy, Y., Wallenburg, A.: Tokeneer: Beyond formal program verification. Embedded Real Time Software and Systems 24 (2010)
* [23] Osherove, R.: The Art of Unit Testing: With Examples in .Net. Manning Publications Co. (2009)
* [24] Rakamaric, Z., Emmi, M.: SMACK: Decoupling Source Language Details from Verifier Implementations. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 106–113. Springer (2014)
* [25] Serebryany, K.: libFuzzer: A library for coverage-guided fuzz testing, https://llvm.org/docs/LibFuzzer.html

##  Appendix 0.A Description of Specification Bugs Found

In this section, we describe the bugs that we have found in the unit proofs of
aws-c-common.

###  0.A.1 Representation Invariant of byte_buf

#### File.

{source/byte_buf.c}xspace \paragraph{Description.}The bug is in the
representation invariant of the {byte_buf}xspacedata structure. The code is
shown in LABEL:fig:byte_buf_is_valid, and the revision is shown in the
comment. The {byte_buf}xspacedata structure contains a field
{buffer}xspacethat points to a writable memory region of size at least
{capacity}xspace.In the representation invariant, {len}xspacewas used instead
of {capacity}xspace.This allows for {buffer}xspaceto be {NULL}xspacewhen
{len}xspaceis $0$ and {capacity}xspaceis not zero. The buggy specification is
_not_ an invariant. We showed that it is not maintained by the API of
{byte_buf}xspace. Therepresentation invariant is used both as pre- and post-
condition in unit proofs, and also in unit tests. The buggy version is weaker
than the correct one. Thus, it is true of any correct instance of
{byte_buf}xspace.For this reason, it is the bug that has not been detected by
unit tests.

#### Story.

According to GitHub logs, the bug was in the code for at least two years. We
found it indirectly using vacuity in SeaHorn. We have initially modelled
memory allocation (i.e., calls to {malloc}xspace)as never failing. That is,
never returning a {NULL}xspacepointer. Under this assumption, some post-
conditions became vacuous. We have then re-defined {malloc}xspaceto non-
deterministically fail. This caused one of the unit proofs that was using this
representation invariant to fail with a counterexample. Examining the
counterexample manually lead to the discovery of the bug. The bug was reported
to AWS. It has pointed to a deeper issue of how {malloc}xspaceshould be
modelled. This resulted in review of all CBMC-based proofs at AWS with
numerous issues uncovered and fixed. The bug is fixed in aws-c-common in
commit ec70687666https://github.com/awslabs/aws-c-common/pull/686..

⬇ 1bool aws_byte_buf_is_valid(const struct aws_byte_buf *const buf) { 2 return
buf != NULL && 3 ((buf->capacity == 0 && buf->len == 0 && buf->buffer == NULL)
|| 4 (buf->capacity > 0 && buf->len <= buf->capacity && 5
AWS_MEM_IS_WRITABLE(buf->buffer, buf->len /* buf->capacity */))); 6}

Figure 10: Representation invariant of
{{{aws_byte_buf}xspace.label{fig:byte_buf_is_valid}}}

###  0.A.2 Bug in verification helper {{{assert_bytes_match}xspace}}

#### File.

{verification/cbmc/sources/utils.c}xspace \paragraph{Description.}The bug in
verification library function that checks that two byte regions are
equivalent. The bug and the revision (in comments) are shown in
LABEL:fig:assert_bytes_match. This function is used to compare content of
zero-terminated strings with non-zero terminated byte buffers. A zero sized
string is not {NULL}xspace(it needs one character for the zero-terminator). A
zero sized byte buffer is {NULL}xspacebecause aws-c-common ensures that
allocating 0 bytes returns {NULL}xspace.Thus, the buggy version of the
function returns false when comparing an empty string with an empty byte
buffer. This contradicts the name and the use of the function in unit proofs.

#### Story.

According to GitHub logs, the bug was in the code for at least two years. We
found the bug by allowing {malloc}xspaceto fail and return {NULL}xspacenon-
deterministically. This enabled code paths in existing unit proofs are
infeasible under previous assumptions. This caused some unit proofs to fail.
Examining the counterexamples manually lead to discovery of this bug.

⬇ 1void assert_bytes_match(const uint8_t *const a, 2 const uint8_t *const b,
const size_t len) { 3 assert(/* len == 0 || */ !a == !b); 4 if (len > 0 && a
!= NULL && b != NULL) { 5 size_t i; 6 /* prevent spurious pointer overflows */
7 __CPROVER_assume(i < len && len < MAX_MALLOC); 8 assert(a[i] == b[i]); 9 }
10}

Figure 11: Verification library function
{{{assert_bytes_match}xspace.label{fig:assert_bytes_match}}}

###  0.A.3 Post-condition bug in unit proof for
{{{aws_mul_size_checked_harness.c}xspace}}

#### File.

{verification/cbmc/proofs/aws_mul_size_checked/}xspace\\\\\code{aws_mul_size_checked_harness.c}
\paragraph{Description.}The bug is in the post-condition of the unit proof.
The bug and the revision (in comments) are shown in
LABEL:fig:aws_mul_size_checked. The function {aws_mul_size_checked}xspaceis a
checked overflow multiplication. If the multiplication does not overflow, the
result of the multiplication is stored in {r}xspace,otherwise, the function
returns an error code. The assertion at line 16 is intended to check for
overflow, but instead, it checks for overflow of addition. The verification
environment is restricted at line 9 to two special values. The post-condition
happens to be true for these two inputs.

#### Story.

The comments in the unit proof restrict the environment because of scalability
issues. This was not a problem for SeaHorn. When migrating, we have removed
the assumption at line 9 and found a counterexample. The bug was fixed by AWS
team as shown in the commented assertion at line 16. The revision, arguably,
creates a different bug. When the code if aws-c-common is compiled for CBMC,
it redefines {aws_mul_u64_checked}xspacewith a call to
{__CPROVER_overflow_mult}xspace.Thus, this unit proof does not check any
actual executable code in the library. The library provides several
implementations of checked arithmetic. The most common one uses checked
arithmetic builtins provided by both Clang and GCC compilers, and others rely
on inline assembly. In SeaHorn, we verify the version that is compiled using
compiler builtins. Thus, with a similar unit proof, SeaHorn is able to check
correctness of the actual implemented code.

⬇ 1#include <aws/common/math.h> 2extern int nondet_int(void); 3extern uint64_t
nondet_uint64_t(void); 4void aws_mul_size_checked_harness() { 5 /* 6 * In this
particular case, full range of nondet inputs leads 7 * to excessively long
runtimes, so use 0 or UINT64_MAX instead. 8 */ 9 uint64_t a = (nondet_int()) ?
0 : UINT64_MAX; 10 uint64_t b = nondet_uint64_t(); 11 uint64_t r =
nondet_uint64_t(); 12 if (!aws_mul_u64_checked(a, b, &r)) { 13 assert(r == a *
b); 14 } else { 15 assert((b > 0) && (a > (UINT64_MAX - b))); 16 /*
assert(__CPROVER_overflow_mult(a, b)); 17 } 18}*/

Figure 12: Unit proof for
{{{aws_mul_size_checked}xspace.label{fig:aws_mul_size_checked}}}

###  0.A.4 Post-condition bug in unit proof for {s_swap}xspaceof priority
queue

#### File.

{verification/cbmc/proofs/aws_priority_queue_s_swap/}xspace\\\\\code{aws_priority_queue_s_swap_harness.c}
\paragraph{Description.}The bug is in one of the post-conditions of the
function {s_swap}xspacethat is used in the implementation of the priority
queue data structure. The complete unit proof is too long to reproduce here,
so we present a relevant snippet in 13 instead. Since the function
{s_swap}xspace isprivate to the priority queue translation unit, a special
syntax is used to call it directly from the unit proof (line 4). The bug is in
the condition of the if-statement at line 8. Conjunction is used instead of
disjunction. The revision is shown in comments and corresponds to the comment
at line 6.

#### Story.

The bug was found by vacuity detection. The assertions inside the function
{assert_array_list_equivalence}xspaceare unreachable. The bug has been
reported, but is not yet fixed. GitHub logs show that the bug has been active
for at least two years. The coverage results from CBMC show that the call to
{assert_array_list_equvalence}xspaceis not covered (i.e., not executed by the
unit proof). However, this seems to have been missed. ⬇ 1void
aws_priority_queue_s_swap_harness() { 2 ... 3 /* Perform operation under
verification */ 4 __CPROVER_file_local_priority_queue_c_s_swap(&queue, a, b);
5 ... 6 /* All the elements in the container except for a and b should stay 7
unchanged */ 8 size_t ob_i = old_byte.index; 9 if ((ob_i < a * item_sz && /*
|| */ ob_i >= (a + 1) * item_sz) && 10 (ob_i < b * item_sz && /* || */ ob_i >=
(b + 1) * item_sz)) { 11 assert_array_list_equivalence(&queue.container, &old,
&old_byte); 12 } 13 ... 14} Figure 13: Snippet of the unit proof for
{s_swap}xspaceof priority queue.

###  0.A.5 Pre-condition bug mixing different kinds of strings

#### File.

{verification/cbmc/proofs/aws_hash_callback_string_eq/}xspace\\\
\code{hash_callback_string_eq_harness.c} \paragraph{Description.}The aws-c-
common library supports two types of strings. The zero-terminated strings from
LibC that are common in C, and its own data structures {aws_string}xspace.The
harness shown in LABEL:fig:aws_hash_callback_string assumes that the
{aws_string}xspaceobject satisfies the C-string representation invariant. The
representation invariant for C-strings happens to be very weak (essentially
that the pointer is not null). According to the C semantics, conversion from a
data structure to a C-string is always possible.

#### Story.

The bug was found during compilation in an IDE. Compilation warnings indicated
that an explicit cast is desirable for the calls to
{aws_c_string_is_valid}xspace.It is clear that the intended specification is
to assume representation invariant for {aws_string}xspaceinstead.

⬇ 1void aws_hash_callback_string_eq_harness() { 2 const struct aws_string
*str1 = ...; 3 const struct aws_string *str2 = ...; 4 5
__CPROVER_assume(aws_c_string_is_valid(str1)); 6
__CPROVER_assume(aws_c_string_is_valid(str2)); 7 /*
__CPROVER_assume(aws_string_is_valid(str1)); */ 8 /*
__CPROVER_assume(aws_string_is_valid(str2)); */ 9 10 11 12 bool rval =
aws_hash_callback_string_eq(str1, str2); 13 if (rval) { 14 assert(str1->len ==
str2->len); 15 assert_bytes_match(str1->bytes, str2->bytes, str1->len); 16 }
17}

Figure 14: Snippet of the unit proof for
{{{aws_hash_callback_string_eq}xspace.label{fig:aws_hash_callback_string}}}

###  0.A.6 Specification stub of hash_iter_delete

#### File.

{verification/cbmc/stubs/aws_hash_iter_overrides.c}xspace
\paragraph{Description.}A bug in _specification stub_ that we have found in
this case study is in the stubbed version of {hash_iter_delete}xspace.The code
is shown in LABEL:fig:hash_iter_delete, and the revision is shown in the
comment at line 8. After deleting an item from the iterator, the specification
stub did not update the {hash_table_state}xspaceof the hash table properly
since the stub did not decrease the {entry_count}xspacefield of it.

#### Story.

We found the bug in an attempt to use original functions over specification
stubs in order to build a more precise proof of {hash_table_foreach}xspace.The
function {hash_table_foreach}xspaceleverages
{hash_iter_begin}xspace,{hash_iter_next}xspaceand {hash_iter_done}xspaceto
iterate over all entries in an {aws_hash_table}xspace.In each iteration,
{hash_iter_delete}xspaceis conditionally invoked to delete an entry from the
table. When we used the original {hash_iter*}xspacefunctions in the SeaHorn
unit proof of {hash_iter_foreach}xspace,we found that the representation
invariant of {aws_hash_table}xspacecould become false in the post-condition of
{hash_iter_foreach}xspace.A deeper look at the counterexample trace revealed
that the {entry_count}xspacefield became a negative number after a particular
execution of {hash_iter_foreach}xspace. Thereason is two-fold. Firstly, there
are two ways in aws-c-common hash table implementation to determine the number
of entries in {aws_hash_table}xspace.The first one is to explicitly look up
the field {entry_count}xspaceand the second one is to implicitly infer it from
the number of allocated entries that has a non-zero hash code. The original
implementation of {hash_iter*}xspacefunction often use the latter way.
Secondly, the CBMC proof non-deterministically initializes the memory that
contains allocated hash table entry slots, but it does not set any constraint
on the number of allocated entries with non-zero hash codes. When we tried to
use original aws-c-common implementations of {hash_iter*}xspacefunctions in
combination of the initialization process from CBMC proofs, it is possible to
create an {aws_hash_table}xspacewith more entries with non-zero hash codes
than {entry_count}xspace,in which case {hash_iter_delete}xspacecould be
invoked more times than {entry_count}xspaceand decrease the field to a
negative number. The aforementioned behavior constitutes a bug in the pre-
condition part of _CaS_ , which stems from a bug in a specification stub of
key functions invoked by the function under verification.

⬇ 1void aws_hash_iter_delete(struct aws_hash_iter *iter, 2 bool
destroy_contents) { 3 /* Build a nondet iterator, set the required fields, 4
and copy it over */ 5 struct aws_hash_iter rval; 6 rval.map = iter->map; 7
rval.slot = iter->slot; 8 rval.limit = iter->limit - 1; 9 rval.status =
AWS_HASH_ITER_STATUS_DELETE_CALLED; 10 // rval.map->p_impl->entry_count--; 11
*iter = rval; 12}

Figure 15: Specification stub of
{{{hash_iter_delete}xspace.label{fig:hash_iter_delete}}}

###  0.A.7 Undefined behaviour in {{{aws_is_mem_zeroed}xspace}}

#### File.

{include/aws/common/zero.inl}xspace \paragraph{Description.}A snippet of a
buggy implementation of {aws_is_mem_zeroed}xspace is shown in
LABEL:fig:is_mem_zeroed. The function can return false even when the memory
pointed by {buf}xspaceis filled with zeroes. The bug in the memory access in
line 12. The buffer {buf}xspaceis accessed using a pointer to
{uint64_t}xspace.This access is only defined if {buf}xspacewas previously
written with the same type. The code violates the strict aliasing rule of C. A
suggested fix is given in comments. We do not know whether the bug manifests
in the production code. The TBAA alias analysis of LLVM is strong enough to
commute read at line 12 with prior writes to {buf}xspace. \paragraph{Story.}In
aws-c-common, the function is called through a macro expansion of
{AWS_IS_ZEROED}xspace.The macro is used in unit proofs and in the production
code. In CBMC mode, the macro expands to CBMC specific implementation. Thus,
the code of {aws_is_mem_zeroed}xspaceis never seen by CBMC. In SeaHorn, we
analyze the code as it is compiled and this function is used. The bug in the
function causes a post-condition to be violated and counterexample is
generated. Manually examining the counterexample identified the bug.

⬇ 1/** 2 * Returns whether each byte is zero. 3 */ 4AWS_STATIC_IMPL 5bool
aws_is_mem_zeroed(const void *buf, size_t bufsize) { 6 const uint64_t *buf_u64
= (const uint64_t *)buf; 7 const size_t num_u64_checks = bufsize / 8; 8 size_t
i; 9 /* uint64_t val; */ 10 for (i = 0; i < num_u64_checks; ++i) { 11 /*
memcpy(&val, &buf_u64[i], sizeof(val)); */ 12 if (buf_u64[i] /* val */) { 13
return false; 14 } 15 } 16 ... 17}

Figure 16: A snippet of {{{aws_is_mem_zeroed}xspace.label{fig:is_mem_zeroed}}}

##  Appendix 0.B Empirical Results

(a) {{{aws_array_list}xspacelabel{fig:comp_arylst}}}

(b) Others

(c) {{{aws_byte_buffer}xspacelabel{fig:comp_bytebuf}}}

(d) {{{aws_byte_cursor}xspacelabel{fig:comp_bytecursor}}}

(e) Hash

(f) {{{aws_hash_table}xspacelabel{fig:comp_hashtab}}}

(g) {{{aws_linked_list}xspacelabel{fig:comp_linklst}}}

(h) {{{aws_priority_queue}xspacelabel{fig:comp_prioque}}}

(i) {{{aws_ring_buffer}xspacelabel{fig:comp_ringbuf}}}

(j) {{{aws_string}xspacelabel{fig:comp_string}}} (k) Running times for CBMC,
SeaHorn, and KLEE on aws-c-common.

#### Background.

In the experiments, for CBMC we use the original unit proof available at aws-
c-common GitHub repository777https://github.com/awslabs/aws-c-
common/tree/main/verification/cbmc/proofs.. SeaHorn and KLEE use our adapted
unit proofs and our implementation of verification library, including
implementation of {nd_<type>}xspacefunctions and initialization helpers.
Obviously, CBMC uses its internal compiler and pre-processing, while other
tools rely on Clang compiler of LLVM. For CBMC, we measure its total time. For
SeaHorn and KLEE the compilation time is excluded because files are pre-
compiled. The compilation time is insignificant. Finally, for KLEE we had to
severely restrict the sizes of allocated memory. For libFuzzer, we do not show
the running times because the most important result is coverage report. The
details of workflow is shown in Fig. 3.

#### Description.

The results are shown in App. 0.B. They are divided into categories. Each
graph shows unit proofs on the $x$-axis and verification time on the $y$-axis.
The category _Hash_ combines {hash_callback}xspaceand {hash_inter}xspace,and
_Others_ combines {arithmetic}xspaceand {array}xspace. Notethat our
performance comparison must be taken with a grain of salt. We have focused on
developing a methodology to adapt the unit proofs to all the different tools.
In some cases, this required significant change to what is being verified,
both in terms of sizes of data structures considered, and in the properties
checked (especially for built-in checks, such as memory safety). In our
experience, all tools produced useful results. In particular, all the
violations in the specifications have been found using SeaHorn. However, these
differences might have a significant effect on the running time. We leave a
more in-depth study of performance of different techniques on the _same_
verification problems for future work.


# Panoptic-Depth Color Map for Combination of Depth and image segmentation

###### Abstract

Image segmentation and depth estimation are crucial tasks in computer vision,
especially in autonomous driving scenarios. Although these tasks are typically
addressed separately, we propose an innovative approach to combine them in our
novel deep learning network, Panoptic-DepthLab. By incorporating an additional
depth estimation branch into the segmentation network, it can predict the
depth of each instance segment. Evaluating on Cityscape dataset, we
demonstrate the effectiveness of our method in achieving high-quality
segmentation results with depth and visualize it with a color map. Our
proposed method demonstrates a new possibility of combining different tasks
and networks to generate a more comprehensive image recognition result to
facilitate the safety of autonomous driving vehicles.

Index Terms—  Autonomous Driving, Depth Estimation, Panoptic Segmentation,
Segmentation with Depth

##  1 Introduction

Image segmentation is a crucial task in Computer Vision that involves
partitioning camera images into different segments or instances based on the
semantic meaning of each pixel. It has a wide range of applications in fields
such as medical image processing, image processing, and autonomous vehicles.
There are three types of segmentation tasks: semantic, instance, and panoptic
segmentation. Semantic segmentation is equivalent to pixel classification
while each pixel belongs to a semantic category, while instance segmentation
focuses on segmenting out the foreground objects and differentiating different
instances within the scene. The third task, panoptic segmentation, is a
relatively new task that aims to unify semantic and instance segmentation into
a single task by performing semantic segmentation on background pixels and
instance segmentation on foreground pixels.

Another important task in autonomous driving scenarios is depth estimation. It
involves predicting the depth value of each image pixel, where the depth
represents the distance from the camera center to the nearest obstacle. Depth
estimation is particularly essential in autonomous driving as it provides
information for the navigation system to avoid collisions. However, with only
pixel-wise depth information, it is insufficient to distinguish instances in
the scene. Therefore, we propose to combine image segmentation and depth
estimation to predict depth value on the instance level and generate a color
map to visualize the image recognition result. We depict the image tasks
taxonomy we introduced in this section in Fig.1.

Fig. 1: Image task taxonomy. Semantic segmentation classifies each image pixel
into semantic categories. Instance segmentation identifies different instances
within the foreground pixels. Panoptic segmentation combines both instance and
semantic segmentation tasks. Depth estimation evaluates the depth value of
each pixel. Lastly, our proposed segmentation with depth task aims to
integrate depth estimation and panoptic segmentation, producing a color map
that represents the instance-level depth value. Fig. 2: Panoptic-DepthLab
architecture. Based on the Panoptic-DeepLab[1] framework, we extend it by
adding a depth estimation decoder branch to predict depth map. The second
decoder branch is responsible for predicting semantic segmentation result, as
the third branch predict the instance segmentation outcome. To incorporate
depth and segmentation results, we average out the region of each
correspondent segment in a depth map to acquire the instance-level depth
value.

To achieve our proposed task, we introduce Panoptic-DepthLab, an extended
variant of the Panoptic-DeepLab[1] segmentation network. By incorporating an
additional depth estimation branch into the panoptic segmentation network, it
is able to generate segmentation and depth estimation results at the same
time. Subsequently, we fuse the panoptic segmentation and depth estimation
results to generate a color map that represents the depth of each instance.
This color map can provide valuable insights for ensuring safety in autonomous
driving scenarios. We illustrate our proposed Panoptic-DepthLab architecture
in Fig.2.

The rest of the paper is organized as follows. Section 2 presents a related
work review in panoptic segmentation and depth estimation. In section 3, we
describe our proposed method, Panoptic-DepthLab in details. Section 4 reports
our experimental results on the Cityscape dataset. Finally, section 5
concludes the paper.

##  2 Related Works

###  2.1 Panoptic Segmentation

Panoptic segmentation[2], also known as scene parsing, combines the tasks of
semantic and instance segmentation. It involves classifying background pixels
into semantic categories and classifying foreground pixels into individual
instances. Many related works extend well-established instance segmentation
networks by incorporating an additional sementic segmentation branch to
achieve panoptic segmentation. For instance, Panoptic-FPN [3], which is based
on Mask-RCNN[4] network, add a segmentation branch to handle background pixel
categories. Additionally, it utilizes a Feature Pyramid Network (FPN) to
extract detailed features for the segmentation branches.

DeeperLab[5], for other example, adopts the encoder-decoder architecture and
Atrous Spatial Pyramid Pooling(ASPP) of DeepLab[6] and adds an additional
prediction head to predict semantic segments and four other keypoint-based
detections to find instances. The UPSNet[7] architecture is similar to
Panoptic-FPN, which adds an FPN module to the backbone and designs separate
semantic and instance heads for prediction. UPSNet is able to achieves 61.8%
PQ on the Cityscape validation dataset.

Panoptic-DeepLab[1], the network on which our work is based, extends the
DeepLabv3+ network architecture to enable panoptic segmentation. It
incorporates dual-ASPP and dual-decoder modules to produce three outputs:
semantic segmentation, object center prediction, and center offset prediction.
For the instance segmentation branch, Panoptic-DeepLab combines the center
prediction heatmap with pixel offset regression to generate class-agnostic
instances. It then employs a majority-vote algorithm, fusing the instance
predictions with the semantic segmentation result to determine the instance
categories. Panoptic-DeepLab adopts a bottom-up approach to address the
instance segmentation aspect of the task, achieving a PQ (Panoptic Quality)
score of 64.1% on the Cityscape validation set.

In conclusion, these works achieve panoptic segmentation by extending instance
segmentation networks to generate semantic segmentation results for background
pixels. Among these works, Panoptic-DeepLab has demonstrated outstanding
performance. Therefore, we have chosen it to be the basis network for our own
approach, leveraging its superior performance.

###  2.2 Monocular Depth Estimation

Monocular depth estimation is another fundamental task in Computer Vision that
aims to predict the distance of each image pixel from the camera center to the
nearest obstacle using a single camera image as input. Traditional approaches
adopt an encoder-decoder architecture similar to semantic segmentation
networks design. The other line of work intent to model the ordinal
relationship of the depth value. Deep Ordinal Regression Network (DORN) [8]
offers an effective approach by formulating the depth regression problem as an
ordinal regression problem. DORN introduces multiple binary classification
subtasks to infer the depth, where each subtask determines whether the pixel
depth is greater than a specific threshold. The final depth value is obtained
by summing the number of subtasks that predict the pixel to be deeper than
each threshold. Additionally, DORN incorporates the ASPP module to capture
global contextual information and enhance the decoder’s performance. Given the
effectiveness of DORN, we adopt this design and integrate it into our depth
estimation branch.

##  3 Proposed Method

###  3.1 Panoptic-DepthLab

In this section, we introduce Panoptic-DepthLab, our proposed network that
aims to produce segmentation with instance-level depth. By adding a depth
estimation decoder branch to the Panoptic-DeepLab segmentation network, we can
get a unified one-stage network that effectively predict segmentation and
depth map in parallel branches. Additionally, we let the segmentation and
depth branch share the same extracted feature map as input. This design
attempt to increase efficiency and avoid extracting duplicate feature map.
During training, we optimize the whole model, allowing the network to jointly
learn multiple tasks. To combine the predicted depth map with the panoptic
segmentation result, we average the pixel depths within each instance region.
The shared encoder features facilitate efficient end-to-end training.
Specifically, our newly added depth estimation branch follows a similar design
to the semantic segmentation branch. The detailed architecture is illustrated
in Fig 3.

Fig. 3: Architecture of Panoptic-DepthLab. Based on Panoptic-DeepLab, we
introduce an additional decoder branch specifically designed for depth
estimation. The network consists of three branches: semantic segmentation,
instance segmentation, and depth estimation, all utilizing the shared feature
map extracted by the encoder. This unified network allows for end-to-end
training with only single camera image as input. During inference, a post-
processing step combines the segmented regions with depth information.

##  4 Experiments

In this section, we present the detail experimental setting and results of our
Panoptic-DepthLab network, which is built upon the Detectron2[9] platform. We
conduct our experiment on Cityscape[10] dataset, which includes 2975 images
for training and 500 images for validation, where most of the image is shot on
cities street in Germany. The dataset consists of eight background categories
and eleven foreground categories for the panoptic segmentation challenge.

During training, we initialize our network with the pre-trained weights
provided by Panoptic-DeepLab, which were trained on the Cityscape dataset for
90K iterations. Subsequently, we fine-tune the entire network for an
additional 10K iterations after incorporating our additional depth estimation
branch. The training process is conducted on 2 TITAN RTX GPUs, with a batch
size of 14. We employ the Adam optimizer with a learning rate set to 0.001.
Additionally, since Cityscape does not provide ground truth depth estimation,
we generate depth maps by converting the provided disparity map to depth map.

###  4.1 Evaluation Metric

To assess the quality of panoptic segmentation results, Kirillov et al.
introduced a novel metric called Panoptic Quality (PQ) [2]. PQ evaluates the
accuracy of both semantic classification and masks prediction. The PQ for a
class is defined as follows:

$PQ=\overbrace{\frac{\sum_{(p,g)TP}IoU(p,g)}{|TP|}}^{\text{Segmentation
Quality(SQ)}}\times\overbrace{\frac{|TP|}{|TP|+\frac{1}{2}|FP|+\frac{1}{2}|FN|}}^{\text{Recognition
Quality(RQ)}}$ (1)

where $|TP|$, $|FP|$, and $|FN|$ represent the number of true positive, false
positive, and false negative respectively. The first term of the equation 1 is
segmentation quality (SQ), which is the average IoU(Intersection over Union)
of true positives masks. The second term is recognition quality (RQ), which is
the F1 score of classification result.

To evaluate the depth estimation result, we adopt the following metrics:
Relative squared error:

$\text{sqErr}=\frac{1}{N}\sum_{i=1}^{N}(\frac{d^{*}_{i}-d_{i}}{d_{i}})^{2}$
(2)

where $d_{i}$ and $d_{i}^{*}$ represent ground truth depth value and predicted
depth value. And the $N$ represent the number of pixel in image.

Relative absolute error:

$\text{absErr}=\frac{1}{N}\sum_{i=1}^{N}|\frac{d^{*}_{i}-d_{i}}{d_{i}}|$ (3)

Inverse root mean square error:

$\text{IRMSE}=\sqrt{\frac{1}{N}\sum_{i=1}^{N}\left(\frac{1}{d^{*}_{i}}-\frac{1}{d_{i}}\right)^{2}}$
(4)

Scale invariant logarithmic error:

$\text{SILog}=\frac{1}{N}\sum_{i=1}^{N}x_{i}^{2}-\frac{1}{N^{2}}(\sum_{i=1}^{N}x_{i})^{2}$
(5)

where $x_{i}=logd_{i}-logd^{*}_{i}$

Accuracy with threshold:

$\delta_{i}=max(\frac{d_{i}}{d_{i}^{*}},\frac{d_{i}^{*}}{d_{i}})<t$ (6)

where $t\in[1.25,1.25^{2},1.25^{3}]$, It represents the percentage of image
pixels whose depth value ratio with the ground truth is smaller than the given
threshold $t$.

###  4.2 Quantitative Result

We present the Panoptic Quality (PQ) of the Panoptic-DepthLab model tested on
the Cityscape validation dataset in Table 1. Our results show that Panoptic-
DepthLab achieves slightly better performance compared to other panoptic
segmentation networks. This improvement can be attributed to the additional
depth map data available during our fine-tuning training, implicitly giving
more useful information to the segmentation branch.

Table 1: Experimental results of Panoptic-DepthLab on the Cityscape validation set. The metric used is Panoptic Quality (PQ). Semantic Quality (SQ) represents the quality of predicted masks, while Recognition Quality (RQ) represents the classification accuracy. The PQ is calculated as $PQ=SQ\times RQ$. Panoptic-DepthLab performs slightly better than other network on PQ metirc. Methods | PQ | SQ | RQ
---|---|---|---
Panoptic-FPN[3] | 55.4 | 77.9 | 69.3
UPSNet[7] | 60.1 | 80.3 | 73.5
Panoptic-DepthLab | 60.3 | 81.5 | 72.9

To determine the better loss function for our depth estimation branch, we
compared two different loss functions. The first one is the loss function
proposed by DORN[8], which discretizes depth values into intervals based on
uncertainty and formulates the regression problem as multiple binary
classification subtasks. The second loss function is smoothed L1 loss.

The results of our experiments are presented in Table 2 and Table 3.
Surprisingly, we found that smooth L1 loss outperformed DORN’s loss after
training for 10K iterations. This may be attributed to the complexity of the
DORN method, which involves a more complex network structure and a larger
number of additional parameters. In contrast, the smoothed L1 loss proved to
be a more effective and straightforward method for our specific task.

Table 2: Evaluation of depth estimation results produced by Panoptic-DepthLab. Both loss function settings were trained for 10K iterations and tested on the Cityscape validation dataset. Evaluation metrics include relative squared error (sqErrorREL), relative absolute error (absErrorRel), inverse root mean square error (IRMSE), and scale invariant logarithmic error (SILog), which assess the difference between the predicted depth map and the ground truth depth map. Smaller values indicate better performance. Loss | sqErr | absErr | IRMSE | SILog
---|---|---|---|---
DORN[8] | 0.72 | 0.69 | 44.64 | 22.31
L1 | 0.63 | 0.60 | 34.57 | 18.58
Table 3: Evaluation of depth estimation results produced by Panoptic-DepthLab. Both loss function settings were trained for 10K iterations and tested on the Cityscape validation dataset. The evaluation metric is accuracy with threshold, representing the percentage of depth map pixels whose ratio with the ground truth pixels is smaller than the assigned threshold value. Threshold values of 1.25, $1.25^{2}$, and $1.25^{3}$ are used. Higher values indicate better performance. Loss | $\delta_{1}<1.25$ | $\delta_{2}<1.25^{2}$ | $\delta_{3}<1.25^{3}$
---|---|---|---
DORN | 0.27 | 0.49 | 0.68
L1 | 0.30 | 0.61 | 0.82

###  4.3 Qualitative Result

To assess the performance of Panoptic-DepthLab, we visualize inference example
on the Cityscape validation set, presented in Fig 4 and Fig 5. In these
examples, each predicted instance is visually distinguished by its assigned
color based on their depth value. Objects in close proximity appear in vibrant
red, while those with medium distance is colored in green and farther away
objects are colored in cooler shades of blue. Additionally, the background
pixels, such as road, sky, and vegetation, are effectively segmented and
labeled in the resulting output. Each instance is also annotated with its
respective category and depth information, providing a detail understanding of
the scene.

Fig. 4: Inference example of Panoptic-DepthLab on the Cityscape validation
set. Each instance is labeled with a category and a depth value, which
determine the color of each foreground segment. The objects closest to the
camera are colored in red, while the farthest objects are colored in blue. The
background pixel is also segmented by its semantic meaning. Our inference
example shows our network is able to produce high-quality segmentation with
depth. Fig. 5: Inference example of Panoptic-DepthLab on the Cityscape
validation set. Each instance is labeled with a category and a depth value,
which determine the color of each foreground segment. The objects closest to
the camera are colored in red, while the farthest objects are colored in blue.
The background pixel is also segmented by its semantic meaning. Our inference
example shows our network is able to produce high-quality segmentation with
depth.

##  5 Conclusions

In this paper, we have presented a novel approach to combine depth estimation
and image segmentation tasks into a unified framework, resulting in a
informative outcome for autonomous driving scenarios. Our proposed network,
Panoptic-DepthLab, builds upon a panoptic segmentation network with an
encoder-decoder architecture and an ASPP module for capturing global context.
We have further extended the network by incorporating an additional depth
prediction branch. The fusion of panoptic segmentation and depth estimation
results is achieved by averaging the pixel depths within each instance region,
enabling comprehensive scene understanding. The effectiveness of our method
has been evaluated on the Cityscape dataset, demonstrating high-quality
segmentation and depth estimation results.

## References

  * [1] Bowen Cheng, Maxwell D Collins, Yukun Zhu, Ting Liu, Thomas S Huang, Hartwig Adam, and Liang-Chieh Chen,  “Panoptic-deeplab: A simple, strong, and fast baseline for bottom-up panoptic segmentation,”  in Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, 2020, pp. 12475–12485.
  * [2] Alexander Kirillov, Kaiming He, Ross Girshick, Carsten Rother, and Piotr Dollár,  “Panoptic segmentation,”  in Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2019, pp. 9404–9413.
  * [3] Alexander Kirillov, Ross Girshick, Kaiming He, and Piotr Dollár,  “Panoptic feature pyramid networks,”  in Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, 2019, pp. 6399–6408.
  * [4] Kaiming He, Georgia Gkioxari, Piotr Dollar, and Ross Girshick,  “Mask r-cnn,”  in Proceedings of the IEEE International Conference on Computer Vision (ICCV), Oct 2017.
  * [5] Tien-Ju Yang, Maxwell D Collins, Yukun Zhu, Jyh-Jing Hwang, Ting Liu, Xiao Zhang, Vivienne Sze, George Papandreou, and Liang-Chieh Chen,  “Deeperlab: Single-shot image parser,”  arXiv preprint arXiv:1902.05093, 2019.
  * [6] Liang-Chieh Chen, Yukun Zhu, George Papandreou, Florian Schroff, and Hartwig Adam,  “Encoder-decoder with atrous separable convolution for semantic image segmentation,”  in Proceedings of the European conference on computer vision (ECCV), 2018, pp. 801–818.
  * [7] Yuwen Xiong, Renjie Liao, Hengshuang Zhao, Rui Hu, Min Bai, Ersin Yumer, and Raquel Urtasun,  “Upsnet: A unified panoptic segmentation network,”  in Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2019, pp. 8818–8826.
  * [8] Huan Fu, Mingming Gong, Chaohui Wang, Kayhan Batmanghelich, and Dacheng Tao,  “Deep ordinal regression network for monocular depth estimation,”  in Proceedings of the IEEE conference on computer vision and pattern recognition, 2018, pp. 2002–2011.
  * [9] Yuxin Wu, Alexander Kirillov, Francisco Massa, Wan-Yen Lo, and Ross Girshick,  “Detectron2,” https://github.com/facebookresearch/detectron2, 2019\.
  * [10] Marius Cordts, Mohamed Omran, Sebastian Ramos, Timo Rehfeld, Markus Enzweiler, Rodrigo Benenson, Uwe Franke, Stefan Roth, and Bernt Schiele,  “The cityscapes dataset for semantic urban scene understanding,”  in Proceedings of the IEEE conference on computer vision and pattern recognition, 2016, pp. 3213–3223.