.

# Rely-guarantee Reasoning about Concurrent Memory Management: Correctness,
Safety and Security

Yongwang Zhao  Zhejiang UniversitySchool of Cyber Science and Technology,
College of Computer Science and Technology38 Zheda
RoadHangzhouZhejiangChina310007 and  David Sanán  Nanyang Technological
UniversitySchool of Computer Science and Engineering50 Nanyang
AvenueSingaporeSingapore639798

###### Abstract.

Formal verification of concurrent operating systems (OSs) is challenging, in
particular the verification of the dynamic memory management due to its
complex data structures and allocation algorithm. An incorrect specification
and implementation of the memory management may lead to system crashes or
exploitable attacks. This article presents the first formal specification and
mechanized proof of a concurrent memory management for a real-world OS
concerning a comprehensive set of properties, including functional
correctness, safety and security. To achieve the highest assurance evaluation
level, we develop a fine-grained formal specification of the Zephyr RTOS buddy
memory management, which closely follows the C code easing validation of the
specification and the source code. The rely-guarantee-based compositional
verification technique has been enforced over the formal model. To support
formal verification of the security property, we extend our rely-guarantee
framework PiCore by a compositional reasoning approach for integrity. Whilst
the security verification of the design shows that it preserves the integrity
property, the verification of the functional properties shows several
problems. These verification issues are translated into finding three bugs in
the C implementation of Zephyr, after inspecting the source code corresponding
to the design lines breaking the properties.

Rely-guarantee, Concurrent OS Kernel, Formal Verification, Memory Management,
Isabelle/HOL

††copyright: acmcopyright††journal: TOSEM††journalyear: 2020††journalvolume:
1††journalnumber: 1††article: 1††publicationmonth: 1††doi:
10.1145/1122445.1122456††ccs: Software and its engineering Software
verification††ccs: Theory of computation Program verification††ccs: Software
and its engineering Memory management††ccs: Security and privacy Operating
systems security

##  1\. Introduction

###  1.1. Context and Motivation

Operating systems, and in particular Real Time Operating Systems (RTOS), are a
fundamental component of critical systems. Correctness, safety and security of
systems highly depend on the system’s underlying OS. As a key component of
OSs, the memory management provides ways to dynamically allocate portions of
memory to programs at their request, and to free them for reuse when no longer
needed. The buddy memory allocation technique (Knowlton, 1965) is a memory
allocation algorithm that splits memory into halves or quarters to try to
satisfy a memory request in a best-fit manner. Buddy memory allocation has
been widely applied in OS kernels (e.g. Linux kernel and Zephyr RTOS
111https://www.zephyrproject.org/). Since program variables and data are
stored in the allocated memory, correct, safe and secure memory management is
extremely critical for the whole system. An incorrect specification and
implementation of the memory management may lead to system crashes and
exploitable attacks.

Formal verification has been intensively conducted on OS kernels in recent
years (Klein, 2009; Zhao et al., 2017). Most of these efforts focus on
sequential OS kernels and assume that there is no in-kernel concurrency (e.g.
seL4 (Klein et al., 2014)). Concurrent kernels allow interleaved execution of
kernel/user modules due to user thread preemption, I/O interrupts and
execution in multicore architectures. Some related work studying the building
and verification of concurrent kernels has been covered in (Gu et al., 2016;
Chen et al., 2016; Xu et al., 2016). However, formal verification of
concurrent OS kernels still present several open challenges. For instance,
formal verification in (Chen et al., 2016) concerns kernels with device
drivers using a verification framework that does not support preemptive and
multicore concurrency. As a consequence it is only possible to verify
interrupt handlers for device drivers not sharing data with and non-handler
kernel code.

Formal verification of OS memory management has been studied in CertiKOS
(Vaynberg and Shao, 2012; Gu et al., 2016), seL4 (Klein and Tuch, 2004; Klein
et al., 2009), Verisoft (Alkassar et al., 2008), and in the hypervisors from
(Blanchard et al., 2015; Bolignano et al., 2016). Algorithms and
implementations of dynamic memory allocation have been formally specified and
verified in an extensive number of works (Yu et al., 2003; Fang and
Sighireanu, 2017a; Marti et al., 2006; Su et al., 2016; Fang and Sighireanu,
2017b; Fang et al., 2018). Concurrency is only studied in (Blanchard et al.,
2015; Gu et al., 2016) considering much simpler data structures and algorithms
than our work. Moreover, only (Fang et al., 2018) studies the buddy memory
allocation considering very abstract data structures. Finally, formal
verification of security properties, e.g. integrity and confidentiality, is
still challenging for concurrent OS kernels (Murray et al., 2012; Costanzo et
al., 2016) and has not been studied for concurrent memory management before.
Confidentiality refers to protecting information from being accessed by
unauthorized parties. In general, it is not preserved by memory allocation at
OS level. For instance, in Zephyr the memory release by a thread does not
clear the allocated memory and the information may be accessed by other
threads. Thus, we consider the integrity of concurrent memory management in
this article, which means the allocated memory of a thread cannot be altered
by other threads.

This article concentrates on the formal specification and formal verification
of functional correctness, safety and security properties on the concurrent
buddy memory management of Zephyr. _Zephyr_ is an open-source state of the art
RTOS managed by the Linux Foundation for connected, resource-constrained
devices, and built with security and safety design in mind. It has been
deployed in IoT gateways, safety shoes, and smart watches, etc. It uses a
buddy memory allocation algorithm optimized for RTOS and is completely
concurrent in the kernel that allows multiple threads to concurrently
manipulate shared memory pools with fine-grained locking. We apply the PiCore
rely-guarantee framework (Zhao et al., 2019a) to the verification of Zephyr.
The compositionality of rely-guarantee allows makes possible to handle the
complexity of the memory allocation algorithm used in Zephyr, and of its data
structures.

###  1.2. Challenges

Formal verification of concurrent memory management, in particular the buddy
memory allocation in Zephyr, is a challenging work.

  1. (1)

_Fine-grained concurrency of the execution of the memory services and of the
shared memory structure_ : On one hand, thread preemption and interruption
make the kernel execution of memory services to be concurrent. Memory
allocation usually uses fine-grained locking for threads. When manipulating a
shared memory pool, memory services in a thread lock the pool by disabling
interruptions inside critical sections as small as possible. On the other
hand, memory pools are shared by threads in a fine-grained parts of its
structure. When a thread is splitting a memory block into smaller ones to get
a suitable block size, another thread may be coalescing partner blocks in the
same pool into a larger one. That is, a thread is manipulating a block sub-
tree of a memory pool, meanwhile another thread is manipulating another block
sub-tree of the same pool.

  2. (2)

_Complex data structure and algorithm of buddy memory management_ : to achieve
high performance, data structures and algorithms in Zephyr are laid out in a
complex manner. First, the buddy memory allocation can split large blocks into
smaller ones, allowing blocks of different sizes to be allocated and released
efficiently while limiting memory fragmentation concerns. Seeking performance,
Zephyr uses a multi-level structure where each level has a bitmap and a linked
list of free memory blocks. The levels of bitmaps actually form a forest of
quad trees of bits. Memory addresses are used as a reference to memory blocks,
so the algorithm has to deal with address alignment and computation concerning
the block size at each level, increasing the complexity of its verification.
Second, the allocation algorithm supports various temporal modes. If a block
of the desired size is unavailable, a thread can optionally wait for one to
become available. There are three different modes for waiting threads: waiting
forever, waiting for a time out, and no wait. Before a thread changes its
state to waiting, it invokes rescheduling in the allocation service and thus
is preempted by ready threads. The system must guarantee that each service
eventually returns from each of the waiting modes.

  3. (3)

_Verification of safety and security of concurrent memory management is
difficult_ : first, a complex algorithm and data structures implies as well
complex invariants over them, that the formal model must preserve as
functional safety properties. These invariants have to guarantee the multi-
level well-shaped bitmaps and their consistency to multi-level free lists. To
prevent memory leaks and block overlapping, a precise reasoning shall keep
track of both numerical and shape properties. Second, as a security property
we verify the integrity of allocated memory blocks among threads, i.e. one
thread can not modify blocks allocated by other threads. In this context,
formal verification of integrity on OS kernels needs to consider the system
events (e.g. kernel services, interrupt handlers), and hence integrity is seen
as a property of state-event based information-flow security (IFS) (Murray et
al., 2012; Costanzo et al., 2016). Works on state-event IFS (Rushby, 1992; von
Oheimb, 2004; Murray et al., 2012) tackle sequential systems and can not be
applied either on the verification concurrent OS kernels. Although there are
some work related to the verification of concurrent IFS (Mantel et al., 2011;
Murray et al., 2016; Murray et al., 2018), these focus on language-based IFS
which can not be used on the verification of integrity for a concurrent
operating system. Therefore the verification of state-event IFS is still an
open challenge.

###  1.3. Approach and Contributions

The safety and security properties in this article concern the small steps
inside memory services that must be preserved by any internal step of the
services. For instance, in the case of Zephyr RTOS, a safety property is that
memory blocks do not overlap each other even during internal steps of the
allocation and release services. It is therefore necessary to find a
verification approach that allows to reason at such fine-grained detail.

In this article, we apply the rely-guarantee reasoning technique to verify the
Zephyr concurrent memory management. This work uses PiCore (Zhao et al.,
2019a), a two-level event-based rely-guarantee framework in Isabelle/HOL for
the specification and verification of concurrent reactive systems (CRS).
PiCore has support for concurrent OSs features like modelling shared-variable
concurrency of multiple threads, interruptable execution of handlers, self-
suspending threads, and rescheduling.

PiCore separates the specification and verification at two levels. The top
level introduces the notion of “events” into the rely-guarantee method for
system reactions. This level defines the events composing a system, and how
and when they are triggered. It supports reactive semantics of interrupt
handlers (e.g. kernel services, scheduler) in OSs, which makes formal
specification of OSs much simpler than those represented by pure programs
(e.g. in (Andronick et al., 2015)). The second level focuses on the
specification and reasoning of the behaviour of the events composing the first
level. PiCore parametrizes the second level using a rely-guarantee interface,
allowing to easily reuse existing rely-guarantee frameworks of imperative
programs. PiCore concurrent constructs allow the specification of Zephyr
multi-thread interleaving, fine-grained locking, and thread preemption.
Compositionality of rely-guarantee makes feasible to prove the functional
correctness of Zephyr and invariants over its data structures.

In this article, we first formalize the data structures of Zephyr memory pools
in Isabelle/HOL, and we analyze its structural properties. The properties
clarify the constraints and consistency of quad trees, free block lists,
memory pool configuration, and waiting threads. These properties conforms the
safety of the memory management. They are defined as invariants for which its
preservation under the execution of services is formally verified. The set of
properties is comprehensive for buddy memory allocation since we can derive
the memory separation property at the memory-block level as discussed below
from them.

Second, we consider memory separation as the security of Zephyr at two levels:
memory-block level and thread level. At the memory-block level, memory
separation ensures that the memory blocks of a memory pool cover the whole
memory address of the pool, but do not overlap each other. This property is
necessary to prevent memory leaks and can be derived from well-shaped
properties of quad trees defined in the invariants. For memory separation at
the thread level, we consider the aforementioned memory integrity among
threads. To tackle this, we extend PiCore with a compositional reasoning
approach for integrity on event-based concurrent systems. This approach
redefines the concept of integrity in terms of fine-grain semantics and it
uses rely-guarantee, as in the core of PiCore, for reasoning on the integrity
of the events by means of observable equivalence among threads.

Third, together with the formal verification of Zephyr, we aim at the highest
evaluation assurance level (EAL 7) of Common Criteria (CC) (Criteria, 2017),
which was declared in the last year as the candidate standard for security
certification by the Zephyr project. Therefore, we develop a fine-grained low
level formal specification of a buddy memory management. The specification
closely follows the Zephyr C code, and thus is able to do the _code-to-spec_
review required by the EAL 7 evaluation, covering all the data structures and
imperative statements present in the implementation. The functional
correctness of the memory management is specified by pre and post conditions
of each service and compositionally proved by the rely-guarantee proof system
of PiCore.

Finally, we enforce the formal verification of functional correctness,
invariant preservation, and memory separation by using the extended rely-
guarantee proof system of PiCore. It supports total correctness for loops
where fairness does not need to be considered. The formal verification shows
the preservation of memory integrity, however, revealed three functional and
safety bugs in the C code: an incorrect block split, an incorrect return from
the kernel services, and non-termination of a loop. Two of them are critical
and have been repaired in the latest release of Zephyr. The third bug causes
nontermination of the allocation service when trying to allocate a block of a
larger size than the maximum allowed.

To the best of our knowledge, this article presents the first formal
specification and mechanized proof of correctness, safety and security for
concurrent memory allocation of a realistic operating system. The formal
specification and proofs in this article are completely developed in
Isabelle/HOL. All the Isabelle/HOL sources are available at
https://lvpgroup.github.io/tosem2021/. We summarize the main contributions of
this article as follows.

  1. (1)

A comprehensive set of critical properties for concurrent buddy memory
management, including functional correctness, safety by invariants, and
security by memory separation. In particular, we clarify the constraints and
consistency of the complicated structure of buddy memory pools.

  2. (2)

The first compositional reasoning approach for state-event based integrity,
its application on a concurrent OS kernel, and its formal proof for the Zephyr
concurrent memory management.

  3. (3)

The first verified formal specification for concurrent buddy memory
allocations which corresponds to the low-level design specification in CC EAL
7 evaluation.

  4. (4)

Critical bugs founds on the functional correctness and safety in Zephyr C
code, which have been repaired in the latest release of Zephyr.

###  1.4. Roadmap

Figure 1. Outline of Main Results

Fig. 1 summarizes the main results presented in this article. First, Section 2
presents the preliminaries of this article including the buddy memory
management in Zephyr (Section 2.1) and our previous PiCore framework (Section
2.2). In Section 3, we formalize the memory data structures, and the safety
and security properties of buddy memory pools. We define the memory structures
in Section 3.1, the invariant properties in Section 3.2, and the memory
separation properties in Section 3.3. The formal specification of memory
allocation and release services of Zephyr is presented in Section 4. For the
compositional verification of security for Zephyr, we propose a security
property _integrity_ for PiCore specifications in Section 5.2 and we discuss
the compositional verification approach in Section 5.3. In Section 6, we show
the rely-guarantee proofs of Zephyr. We first give the correctness
specification by rely-guarantee conditions in Section 6.1, which is embedded
with the invariant and memory separation properties. We then present the proof
of partial correctness (Section 6.2), termination (Section 6.3), safety
(Section 6.4) and security (Section 6.5) of the memory services.

This article is an extension of our previous paper (Zhao and Sanán, 2019).
Compared to (Zhao and Sanán, 2019), (1) we add security properties about
memory separation at memory-block level and thread level in this article; (2)
we present the invariants in a more comprehensive and formal way; (3) for
memory separation in concurrent settings, we extend our PiCore framework (Zhao
et al., 2019a) by a compositional verification approach of integrity, and then
we apply the new PiCore framework to the rely-guarantee reasoning of Zephyr
RTOS; (4) we add security proof and present more comprehensive proofs of
correctness and safety in this article; (5) finally, we add comparison to
related work and present the limitation and discussion of our work.

##  2\. Preliminaries

###  2.1. Concurrent Memory Management in Zephyr RTOS

In Zephyr, a memory pool is a kernel object that allows memory blocks to be
dynamically allocated, from a designated memory region, and released back into
the pool. Its C code implementation is shown in the left part of Fig. 2. The
right part of this figure shows the formalization of the memory pool, which
will be discussed in next section. A memory pool’s buffer ($*buf$) is an
$n\\_max$-size array of blocks of $max\\_sz$ bytes at level $0$, with no
wasted space between them. The size of the buffer is thus $n\\_max\times
max\\_sz$ bytes long. Zephyr tries to accomplish a memory request by splitting
available blocks into smaller ones fitting as best as possible the requested
size. Each “level 0” block is a quad-block that can be split into four smaller
“level 1” blocks of equal size. Likewise, each level 1 block is itself a quad-
block that can be split again. At each level, the four smaller blocks become
_buddies_ or _partners_ to each other. The block size at level $l$ is thus
$max\\_sz/4^{l}$.

⬇

struct k_mem_block_id {

u32_t pool : 8;

u32_t level : 4;

u32_t block : 20;

};

struct k_mem_block {

void *data;

struct k_mem_block_id id;

};

struct k_mem_pool_lvl {

union {

u32_t *bits_p;

u32_t bits;

};

sys_dlist_t free_list;

};

struct k_mem_pool {

void *buf;

size_t max_sz;

u16_t n_max;

u8_t n_levels;

u8_t max_inline_level;

struct k_mem_pool_lvl *levels;

_wait_q_t wait_q;

};

_typedef_ mempool-ref  _$=$_ ref

_type -synonym_ mem-ref  _$=$_ nat

_record_ Mem-block  _$=$_ pool  _$\mathord{:}$__$\mathord{:}$_ mempool-ref

level  _$\mathord{:}$__$\mathord{:}$_ nat

block  _$\mathord{:}$__$\mathord{:}$_ nat

data  _$\mathord{:}$__$\mathord{:}$_ mem-ref

_datatype_ BlockState  _$=$_ ALLOCATED  _$\mid$_ FREE  _$\mid$_ DIVIDED
_$\mid$_

NOEXIST  _$\mid$_ FREEING  _$\mid$_ ALLOCATING

_record_ Mem-pool-lvl  _$=$_

bits  _$\mathord{:}$__$\mathord{:}$_ BlockState list

free-list  _$\mathord{:}$__$\mathord{:}$_ mem-ref list

_record_ Mem-pool  _$=$_ buf  _$\mathord{:}$__$\mathord{:}$_ mem-ref

max-sz  _$\mathord{:}$__$\mathord{:}$_ nat

n-max  _$\mathord{:}$__$\mathord{:}$_ nat

n-levels  _$\mathord{:}$__$\mathord{:}$_ nat

levels  _$\mathord{:}$__$\mathord{:}$_ Mem-pool-lvl list

wait-q  _$\mathord{:}$__$\mathord{:}$_ Thread list

Figure 2. Data Structure of Memory Pool in Zephyr v1.8.0 and Its Formalization

The pool is initially configured with the parameters $n\\_max$ and $max\\_sz$,
together with a third parameter $min\\_sz$. $min\\_sz$ defines the minimum
size for an allocated block and must be a multiple of four, i.e., there exists
an $X>0$ such that $\min\\_sz=4\times X$. Memory pool blocks are recursively
split into quarters until blocks of the minimum size are obtained, at which
point no further split can occur. The depth at which $min\\_sz$ blocks are
allocated is $n\\_levels$ and satisfies that $n\\_max=min\\_sz\times
4^{n\\_levels}$.

Every memory block is composed of a $level$; a $block$ index within its level,
ranging from $0$ to $(n\\_max\times 4^{level})-1$; and the $data$ as a pointer
to the block start address, which is equal to $buf+(max\\_sz/4^{level})\times
block$. We use the tuple $(level,block)$ to uniquely represent a block within
a pool $p$.

A memory pool keeps track of how its buffer space has been split using a
linked list _free_list_ with the start address of the free blocks in each
level. To improve the performance of coalescing partner blocks, memory pools
maintain a bitmap at each level to indicate the allocation status of each
block in the level. This structure is represented by a C union of an integer
_bits_ and an array _bits_p_. The implementation can allocate bitmaps at
levels smaller than $max\\_inlinle\\_levels$ using only an integer _bits_.
However, the number of blocks in levels higher than $max\\_inlinle\\_levels$
make necessary to allocate the bitmap information using the array _bits_map_.
In such a design, the levels of bitmaps actually form a forest of complete
quad trees. The bit $i$ in the bitmap of level $j$ is set to $1$ for the block
$(i,j)$ iff it is a free block, i.e., it is in the free list at level $i$.
Otherwise, the bitmap for such block is set to $0$.

⬇

1static int pool_alloc(struct k_mem_pool *p,struct k_mem_block *block,size_t
size)

2{

3 size_t lsizes[p->n_levels];

4 int i, alloc_l = -1, free_l = -1, from_l;

5 void *blk = NULL;

6 lsizes[0] = _ALIGN4(p->max_sz);

7 for (i = 0; i < p->n_levels; i++) {

8 if (i > 0) { lsizes[i] = _ALIGN4(lsizes[i-1] / 4); }

9 if (lsizes[i] < size) { break; }

10 alloc_l = i;

11 if (!level_empty(p, i)) { free_l = i; }

12 }

13 if (alloc_l < 0 || free_l < 0) {

14 block->data = NULL;

15 return -ENOMEM;

16 }

17 blk = alloc_block(p, free_l, lsizes[free_l]);

18 if (!blk) { return -EAGAIN; }

19 /* Iteratively break the smallest enclosing block... */

20 for (from_l = free_l; level_empty(p, alloc_l) && from_l < alloc_l;
from_l++) {

21 blk = break_block(p, blk, from_l, lsizes);

22 }

23 block->data = blk; block->id.pool = pool_id(p); block->id.level = alloc_l;

24 block->id.block = block_num(p, block->data, lsizes[alloc_l]);

25 return 0;

26}

27

28int k_mem_pool_alloc(struct k_mem_pool *p, struct k_mem_block *block, size_t
size, s32_t timeout)

29{

30 int ret, key;

31 s64_t end = 0;

32

33 if (timeout > 0) { end = _tick_get() + _ms_to_ticks(timeout); }

34 while (1) {

35 ret = pool_alloc(p, block, size);

36 if (ret == 0 || timeout == K_NO_WAIT || ret == -EAGAIN || (ret && ret !=
-ENOMEM)) {

37 return ret;

38 }

39 key = irq_lock();

40 _pend_current_thread(&p->wait_q, timeout);

41 _Swap(key);

42

43 if (timeout != K_FOREVER) {

44 timeout = end - _tick_get();

45 if (timeout < 0) { break; }

46 }

47 }

48 return -EAGAIN;

49}

Figure 3. The C Source Code of Memory Allocation in Zephyr v1.8.0

Zephyr provides two kernel services _k_mem_pool_alloc_ and _k_mem_pool_free_ ,
for memory allocation and release respectively. The main part of the C code of
_k_mem_pool_alloc_ is shown in Fig. 3 in a compact manner. When an application
requests for a memory block, Zephyr first computes $alloc\\_l$ and $free\\_l$
(Lines 7 - 16). $alloc\\_l$ is the level with the size of the smallest block
that will satisfy the request, and $free\\_l$, with $free\\_l\leqslant
alloc\\_l$, is the lowest level where there are free memory blocks. Since the
services are concurrent, when the service tries to allocate a free block _blk_
from level $free\\_l$ (Line 17), blocks at that level may be allocated or
merged into a bigger block by other concurrent threads. In such case the
service will back out (Line 18) and tell the main function _k_mem_pool_alloc_
to retry. If $blk$ is successfully locked for allocation, then it is broken
down to level $alloc\\_l$ (Lines 20 - 22). The allocation service
_k_mem_pool_alloc_ supports a _timeout_ parameter to allow threads waiting for
that pool for a period of time when the call does not succeed. If the
allocation fails (Line 36) and the timeout is not _K_NO_WAIT_ , the thread is
suspended (Line 40) in a linked list _wait_q_ and the context is switched to
another thread (Line 41).

Interruptions are always enabled in both services with the exception of the
code for the functions _alloc_block_ and _break_block_ , which invoke
_irq_lock_ and _irq_unlock_ to respectively enable and disable interruptions.
Similar to _k_mem_pool_alloc_ , the execution of _k_mem_pool_free_ is
interruptable as well.

###  2.2. The PiCore Rely-guarantee Framework

The abstract syntax of the PiCore language (Zhao et al., 2019a) is shown in
Fig. 4. The syntax for events distinguishes basic events pending to be
triggered from already triggered events that are under execution. A basic
event is defined as $\textbf{Event}\ {(l,g,P)}$, where $l$ is the event name,
$g$ the guard condition, and $P$ the body of the event. When $\textbf{Event}\
{(l,g,P)}$ is triggered, its body begins to be executed and it becomes a
triggered event $\lfloor{P}\rfloor$. The execution of $\lfloor{P}\rfloor$ just
simulates the program $P$. Events are parametrized in the meta-logic as
“$\lambda(plist,\kappa).\ \textbf{Event}\ {(l,g,P)}$”, where $plist$ is the
list of input parameters, and $\kappa$ is the event system identifier that the
event belongs to. These parameters are not part of the syntax of events to
make the guard $g$ and the event body $P$, as well as the rely and guarantee
relations, more flexible, allowing to define different instances of the
relations for different values of $plist$ and $\kappa$. Fig. 5 illustrates an
_event_ in the concrete syntax of PiCore. Instead of defining a language for
programs, PiCore reuses existing languages and their rely-guarantee proof
systems.

Event:
---
$\begin{aligned} \mathcal{E}\ ::=&\ \textbf{Event}\ {(l,g,P)}&(Basic\
Event)\\\ |&\ \lfloor{P}\rfloor&(Triggered\ Event)\end{aligned}$
Event System:
$\begin{aligned} \mathcal{S}\ ::=&\ \\{{\mathcal{E}_{0}},\ ...,\
{\mathcal{E}_{n}}\\}&(Event\ Set)\\\ |&\
{\mathcal{E}}\triangleright{\mathcal{S}}&(Event\ Sequence)\end{aligned}$
Parallel Event System:
$\begin{aligned} \mathcal{PS}\ ::=\
\mathcal{K}\rightarrow\mathcal{S}\end{aligned}$
Figure 4. Abstract Syntax of PiCore Language

_EVENT_ alloc [Ref p, Nat size, Int timeout] $@$ $\kappa$

_WHEN_

p  _$\in$_  _´_ mem-pools  _$\wedge$_ timeout  _$\geq$_  _$-$_ 1

_THEN_

……

IF timeout  _$ >$_ 0 THEN

 _´_ endt  _$\mathord{:}$__$=$_  _´_ endt _$($_ t  _$\mathord{:}$__$=$_  _´_
tick  _$+$_ timeout _$)$_

FI;;

……

_END_

Figure 5. An Example of Event in Concrete Syntax

At the system reaction level, PiCore considers a reactive system as a set of
event handlers called _event systems_ responding to stimulus from the
environment. The execution of an event system concerns the continuous
evaluation of guards of the events with their input arguments. From the set of
events for which their associated guard condition holds in the current state,
one event is non-deterministically selected to be triggered, and then its body
is executed. After the event finishes, the evaluation of guards starts again
looking for the next event to be triggered. We call the semantics of event
systems _reactive semantics_ , where the event context shows the event
currently being executed. A CRS is modeled as the _parallel composition_ of
event systems that are concurrently executed.

PiCore supports the verification of two different kinds of properties in the
rely-guarantee proof system for reactive systems: pre and post conditions of
events and invariants in the fine-grained execution of events. A rely-
guarantee specification for a system is a quadruple $RGCond=\langle
pre,R,G,pst\rangle$, where $pre$ is the pre-condition, $R$ is the rely
condition, $G$ is the guarantee condition, and $pst$ is the post-condition.
The intuitive meaning of a valid rely-guarantee specification for a parallel
component $P$, denoted by $\Sigma\models{P}\ \mathbf{sat}\ {\langle
pre,R,G,pst\rangle}$, is that if $P$ is executed from an initial state $s\in
pre$ and any environment transition belongs to the rely relation $R$, then the
state transitions carried out by $P$ belong to the guarantee relation $G$ and
the final states belong to $pst$. $\Sigma$ is used to represent static
configuration of programs like environments for procedure declarations.

We have defined a rely-guarantee axiomatic proof system for the PiCore
specification language to prove validity of rely-guarantee specifications.
Soundness of the proof system with regards to the definition of validity has
been proven in Isabelle/HOL. Some of the rules composing the axiomatic
reasoning system are shown in Fig. 6.

| [Await]
---
$\Sigma\vdash{(\textbf{Await}\ {b}\ {P})}\ \mathbf{sat}\ {\langle
pre,R,G,pst\rangle}\begin{tabular}[]{l}$\Sigma\vdash{P}\ \mathbf{sat}\
{\langle pre\cap b\cap\\{V\\},Id,UNIV,\\{s.\ (V,s)\in G\\}\cap pst\rangle}$\\\
$stable(pre,R)\quad stable(pst,R)$\end{tabular}$
| [BasicEvt]
---
$\Sigma\vdash{\textbf{Event}\ {\alpha}}\ \mathbf{sat}\ {\langle
pre,R,G,pst\rangle}\begin{tabular}[]{l}$\Sigma\vdash{body(\alpha)}\
\mathbf{sat}\ {\langle pre\cap guard(\alpha),R,G,pst\rangle}$\\\
$stable(pre,R)\quad\forall s.\ (s,s)\in G$\end{tabular}$

| [While]
---
$\Sigma\vdash{(\textbf{While}\ {b}\ {P})}\ \mathbf{sat}\ {\langle
loopinv,R,G,pst\rangle}\begin{tabular}[]{l}$\Sigma\vdash{P}\ \mathbf{sat}\
{\langle loopinv\cap b,R,G,loopinv\rangle}$\\\ $loopinv\cap-b\subseteq
pst\quad\forall s.\ (s,s)\in G$\\\ $stable(loopinv,R)\quad
stable(pst,R)$\end{tabular}$
| [Par]
---
$\Sigma\vdash{\mathcal{PS}}\ \mathbf{sat}\ {\langle
pre,R,G,pst\rangle}\begin{tabular}[]{l}$(1)\forall\kappa.\
\Sigma\vdash{\mathcal{PS}(\kappa)}\ \mathbf{sat}\ {\langle
pres_{\kappa},Rs_{\kappa},Gs_{\kappa},psts_{\kappa}\rangle}$\\\
$(2)\forall\kappa.\ pre\subseteq pres_{\kappa}\quad(3)\forall\kappa.\
psts_{\kappa}\subseteq pst\quad(4)\forall\kappa.\ Gs_{\kappa}\subseteq G$\\\
$(5)\forall\kappa.\ R\subseteq
Rs_{\kappa}\quad(6)\forall\kappa,\kappa^{\prime}.\
\kappa\neq\kappa^{\prime}\longrightarrow Gs_{\kappa}\subseteq
Rs_{\kappa^{\prime}}$\end{tabular}$

Figure 6. Subset of Rely-guarantee Proof Rules in PiCore

A predicate $P$ is stable w.r.t. a relation $R$, represented as $stable(P,R)$,
when for any pair of states $(s,t)$ such that $s\in P$ and $(s,t)\in R$ then
$t\in P$. The intuitive meaning is that an environment represented by $R$ does
not affect the satisfiability of $P$. The parallel rule in Fig. 6 establishes
compositionality of the proof system, where verification of the parallel
specification can be reduced to the verification of individual event systems
first and then to the verification of individual events. It is necessary that
each event system $\mathcal{PS}(\kappa)$ satisfies its specification $\langle
pres_{\kappa},Rs_{\kappa},Gs_{\kappa},psts_{\kappa}\rangle$ (Premise 1); the
pre-condition for the parallel composition implies all the event system’s pre-
conditions (Premise 2); the overall post-condition must be a logical
consequence of all post-conditions of event systems (Premise 3); since an
action transition of the concurrent system is performed by one of its event
system, the guarantee condition $Gs_{\kappa}$ of each event system must be a
subset of the overall guarantee condition $G$ (Premise 4); an environment
transition $Rs_{\kappa}$ for the event system $\kappa$ corresponds to a
transition from the overall environment $R$ (Premise 5); and an action
transition of an event system $\kappa$ should be defined in the rely condition
of another event system $\kappa^{\prime}$, where $\kappa\neq\kappa^{\prime}$
(Premise 6).

PiCore considers invariants of CRSs in safety verification. To show that $inv$
is preserved by a system $\mathcal{PS}$, it suffices to show the invariant
verification theorem as follows. This theorem indicates that (1) the system
satisfies its rely-guarantee specification $\langle init,R,G,post\rangle$, (2)
$inv$ initially holds in the set of initial states, and (3) each action
transition as well as each environment transition preserve $inv$. Later,
invariant verification is decomposed to the verification of individual events
by the proof system of PiCore.

###### Theorem 2.1 (Invariant Verification).

For formal specification $\mathcal{PS}$ and $\Sigma$, a state set $init$, a
rely condition $R$, and $inv$, if

  * •

$\Sigma\vdash{\mathcal{PS}}\ \mathbf{sat}\ {\langle init,R,G,post\rangle}$.

  * •

$init\subseteq\\{s.\ inv(s)\\}$.

  * •

$stable(\\{s.\ inv(s)\\},R)$ and $stable(\\{s.\ inv(s)\\},G)$ are satisfied.

then $inv$ is preserved by $\mathcal{PS}$ w.r.t. $init$ and $R$.

##  3\. Defining Structures and Properties of Buddy Memory Pools

This section formalizes the whole data structure of memory pools in Zephyr.
Based on that formalization, we define safety properties as a comprehensive
set of invariants and the security property as a two-level memory separation.
The memory separation at memory-block level can be derived from the invariants
on the memory.

###  3.1. Structure of Memory Pools

As a specification of low-level design, we use abstract data types to
represent the complete structure of memory pools. The formalization of the
memory pool in Zephyr is shown in the right part of Fig. 2. We use an abstract
reference _ref_ in Isabelle to define pointers to memory pools. Starting
addresses of memory blocks, memory pools, and unsigned integers in the
implementation are defined as _natural_ numbers (_nat_). Linked lists used in
the implementation for the elements _levels_ and _free_list_ , together with
the bitmaps used in _bits_ and _bits_p_ , are defined as a _list_ type. C
_structs_ are modelled in Isabelle as _records_ of the same name as the
implementation and comprising the same data. There are two exceptions to this:
(1) $k\\_mem\\_block\\_id$ and $k\\_mem\\_block$ are merged in one single
record, (2) the union in the struct $k\\_mem\\_pool\\_lvl$ is replaced by a
single list representing the bitmap, and thus _max_inline_level_ is removed.

Figure 7. Structure of Memory Pools

Threads may concurrently split and coalesce memory blocks during the execution
of the allocation and realease services. The Zephyr implementation makes use
of a bitmap to represent the state of a memory block. The bit $j$ of the
bitmap for level a $i$ is set to $1$ iff the memory address of the memory
block $(i,j)$ is in the free list at level $i$. A bit $j$ at a level $i$ is
set to $0$ under the following conditions: (1) its corresponding memory block
is allocated (_ALLOCATED_), (2) the memory block has been split (_DIVIDED_),
(3) the memory block is being split in the allocation service (_ALLOCATING_)
(Line 21 in Fig. 3), (4) the memory block is being coalesced in the release
service (_FREEING_), and (5) the memory block does not exist (_NOEXIST_).
Instead of only using a binary representation, our formal specification models
the bitmap using a datatype _BlockState_ that is composed of these cases
together with _FREE_. The reason of this decision is to simplify proving that
the bitmap shape is well-formed. In particular, this representation makes less
complex to verify the case in which the descendant of a free block is a non-
free block. This is the case where the last free block has not been split and
therefore lower levels do not exist. We illustrate a structure of a memory
pool in Fig. 7. The top of the figure shows the real memory of the first block
at level $0$.

###  3.2. Invariant

The structural properties clarify the constraints on and the consistency of
quad trees, free block lists, the memory pool configuration, and waiting
threads. All of them are thought of as invariants on the kernel state and have
been formally verified on the formal specification in Isabelle/HOL.

####  3.2.1. Well-shaped bitmaps

We say that the logical memory block $j$ at a level $i$ physically exists iff
the value of the bitmap $j$ at the level $i$ is _ALLOCATED_ , _FREE_ ,
_ALLOCATING_ , or _FREEING_ , represented by the predicate $is\\_memblock$. We
do not consider blocks marked as _DIVIDED_ as physical blocks since it is only
a logical block containing other blocks. A valid forest is defined by the
following rules: (1) the parent bit of an existing memory block is _DIVIDED_
and its child bits are _NOEXIST_ , denoted by the predicate $noexist\\_bits$
that checks for a given bitmap $b$ and a position $j$ that nodes $b!j$ to
$b!(j+3)$ are set as _NOEXIST_ ; (2) the parent bit of a _DIVIDED_ block is
also _DIVIDED_ ; and (3) the child bits of a _NOEXIST_ bit are also _NOEXIST_
and its parent can not be a _DIVIDED_ block. The property is defined as the
predicate _inv -bitmap_($s$) as follows, where $s$ is the system state of
Zephyr memory management.

_inv -bitmap_ s  _$\equiv$_ _$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_ let mp  _$=$_ mem-pool-info s p in

 _$\forall\,$_ i  _$ <$_ length  _$($_ levels mp _$)$__$\mathord{.}$_ let bts
_$=$_ bits  _$($_ levels mp  _$!$_ i _$)$_ in

 _$($__$\forall\,$_ j  _$ <$_ length bts _$\mathord{.}$_  _$($_
is_memblock(bts  _$!$_ j) _$\longrightarrow$_  _$($_ i  _$ >$_ 0
_$\longrightarrow$_  _$($_ bits  _$($_ levels mp  _$!$_  _$($_ i  _$-$_ 1
_$)$__$)$__$)$_  _$!$_  _$($_ j div 4 _$)$_  _$=$_ DIVIDED _$)$_

_$\wedge$_  _$($_ i  _$ <$_ length  _$($_ levels mp _$)$_  _$-$_ 1
_$\longrightarrow$_ noexist-bits mp  _$($_ i _$+$_ 1 _$)$_  _$($_ j _$*$_ 4
_$)$_  _$)$__$)$_

_$\wedge$_  _$($_ bts  _$!$_ j  _$=$_ DIVIDED  _$\longrightarrow$_ i  _$ >$_ 0
_$\longrightarrow$_  _$($_ bits  _$($_ levels mp  _$!$_  _$($_ i  _$-$_ 1
_$)$__$)$__$)$_  _$!$_  _$($_ j div 4 _$)$_  _$=$_ DIVIDED _$)$_

 _$\wedge$_  _$($_ bts  _$!$_ j  _$=$_ NOEXIST  _$\longrightarrow$_ i  _$ <$_
length  _$($_ levels mp _$)$_  _$-$_ 1 _$\longrightarrow$_ noexist-bits mp
_$($_ i _$+$_ 1 _$)$_  _$($_ j _$*$_ 4 _$)$__$)$_

 _$\wedge$_  _$($_ bts  _$!$_ j  _$=$_ NOEXIST  _$\wedge$_ i  _$ >$_ 0
_$\longrightarrow$_  _$($_ bits  _$($_ levels mp  _$!$_  _$($_ i  _$-$_ 1
_$)$__$)$__$)$_  _$!$_  _$($_ j div 4 _$)$_  _$\not=$_ DIVIDED _$)$_  _$)$_

In Isabelle, _mem_pools s_ captures the set of pools in state $s$, and
_mem_pool_info s p_ gets the memory pool referred by $p$. For a list $l$, _l !
i_ gets the $i$th element.

There are two additional properties on bitmaps. First, the address space of
any memory pool cannot be empty, i.e., the bits at level 0 have to be
different to _NOEXIST_. Second, the allocation algorithm may split a memory
block into smaller ones, but not the those blocks at the lowest level (i.e.
level $n\\_levels-1$), therefore the bits at the lowest level have to be
different than _DIVIDED_ , being invalid if it is divided. The first property
is defined as _inv -bitmap0_($s$) and the second as _inv -bitmapn_($s$).

_inv -bitmap0_ s  _$\equiv$_ _$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_

let bits0  _$=$_ bits  _$($_ levels  _$($_ mem-pool-info s p _$)$_  _$!$_ 0
_$)$_ in  _$\forall\,$_ i _$ <$_length bits0 _$\mathord{.}$_ bits0  _$!$_ i
_$\not=$_ NOEXIST

_inv -bitmapn_ s  _$\equiv$_ _$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_

let bitsn  _$=$_ bits  _$($__$($_ levels  _$($_ mem-pool-info s p _$)$_  _$!$_
_$($_ length  _$($_ levels  _$($_ mem-pool-info s p _$)$__$)$_  _$-$_ 1
_$)$__$)$__$)$_

in  _$\forall\,$_ i _$ <$_length bitsn _$\mathord{.}$_ bitsn  _$!$_ i
_$\not=$_ DIVIDED

####  3.2.2. Consistency of the memory configuration

The configuration of a memory pool is set when it is initialized. Since the
minimum block size is aligned to 4 bytes, there must exist an $n>0$ such that
the maximum size of a pool is equal to $4\times n\times 4^{n\\_levels}$,
relating the number of levels of a level 0 block with its maximum size.
Moreover, the number of blocks at level 0 and the number of levels have to be
greater than zero, since the memory pool cannot be empty. The number of levels
is equal to the length of the pool $levels$ list. Finally, the length of the
bitmap at level $i$ has to be $n\\_max\times 4^{i}$. This property is defined
as _inv -mempool-info_($s$).

_inv -mempool-info_ s  _$\equiv$_  _$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_ let mp  _$=$_ mem-pool-info s p in

 _$($__$\exists\,$_ n _$ >$_0 _$\mathord{.}$_ max-sz mp  _$=$_  _$($_ 4  _$*$_
n _$)$_  _$*$_  _$($_ 4 ^ n-levels mp _$)$__$)$_

 _$\wedge$_ n-max mp  _$ >$_ 0  _$\wedge$_ n-levels mp  _$ >$_ 0 _$\wedge$_
n-levels mp  _$=$_ length  _$($_ levels mp _$)$_

 _$\wedge$_  _$($__$\forall\,$_ i _$ <$_length  _$($_ levels mp
_$)$__$\mathord{.}$_ length  _$($_ bits  _$($_ levels mp  _$!$_ i _$)$__$)$_
_$=$_  _$($_ n-max mp _$)$_  _$*$_ 4 ^ i _$)$_

####  3.2.3. No partner fragmentation

The memory release algorithm in Zephyr coalesces free partner memory blocks
into blocks as large as possible for all the descendants from the root level,
without including it. Thus, a memory pool does not contain four _FREE_ partner
bits. This is checked by the $partner\\_bits$ function. Note that the blocks
of a pool at level 0 should not be coalesced. This property is defined as the
_inv -bitmap-not4free_(s) predicate as follows.

_inv -bitmap-not4free_ s  _$\equiv$_ _$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_ let mp  _$=$_ mem-pool-info s p in

 _$\forall\,$_ i  _$ <$_ length  _$($_ levels mp _$)$__$\mathord{.}$_ let bts
_$=$_ bits  _$($_ levels mp  _$!$_ i _$)$_ in

 _$($__$\forall\,$_ j  _$ <$_ length bts _$\mathord{.}$_ i  _$ >$_ 0
_$\longrightarrow$_  _$\neg$_ partner-bits mp i j _$)$_

####  3.2.4. Validity of free block lists

The free list at one level keeps the starting address of free memory blocks.
The memory management ensures that the addresses in the list are valid, i.e.,
they are different from each other and aligned to the _block size_ , which at
a level $i$ is given by ($max\\_sz/4^{i}$). Moreover, a memory block is in the
free list iff the corresponding bit of the bitmap is _FREE_. This property is
defined as the _inv -bitmap-freelist_(s) predicate as follows.

_inv -bitmap-freelist_ s  _$\equiv$_ _$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_ let mp  _$=$_ mem-pool-info s p in

 _$\forall\,$_ i  _$ <$_ length  _$($_ levels mp _$)$__$\mathord{.}$_ let bts
_$=$_ bits  _$($_ levels mp  _$!$_ i _$)$__$\mathord{;}$_ fl  _$=$_ free-list
_$($_ levels mp  _$!$_ i _$)$_ in

 _$($__$\forall\,$_ j  _$ <$_ length bts _$\mathord{.}$_ bts  _$!$_ j  _$=$_
FREE  _$\longleftrightarrow$_ buf mp  _$+$_ j  _$*$_  _$($_ max-sz mp div
_$($_ 4 ^ i _$)$__$)$_  _$\in$_ set fl _$)$_  _$\wedge$_

 _$($__$\forall\,$_ j  _$ <$_ length fl _$\mathord{.}$_  _$($__$\exists\,$_ n
_$\mathord{.}$_ n  _$ <$_ n-max mp  _$*$_  _$($_ 4 ^ i _$)$_  _$\wedge$_ fl
_$!$_ j  _$=$_ buf mp  _$+$_ n  _$*$_  _$($_ max-sz mp div  _$($_ 4 ^ i
_$)$__$)$__$)$__$)$_ _$\wedge$_ distinct fl

####  3.2.5. Non-overlapping of memory pools

The memory spaces of the set of pools defined in a system must be disjoint, so
the set of memory addresses of a pool does not belong to the memory space of
any other pool. This property is defined as the _inv -pools-notoverlap_(s)
predicate as follows.

_inv -pools-notoverlap_ s  _$\equiv$_ _$($_ _$\forall\,$_ p1 p2
_$\mathord{.}$_ p1 _$\in$_ mem-pools s _$\wedge$_ p1 _$\in$_ mem-pools s
_$\wedge$_ p1 _$\not=$_ p2 _$\longrightarrow$_

_$($__$\nexists\,$_ addr _$\mathord{.}$_ addr  _$\in$_ mempool-addrspace s p1
_$\wedge$_ addr  _$\in$_ mempool-addrspace s p2 _$)$__$)$_

####  3.2.6. Consistency of waiting threads

The state of a suspended thread in _wait_q_ has to be consistent with the
threads waiting for a memory pool. Threads can only be blocked once, and those
threads waiting for available memory blocks have to be in a _BLOCKED_ state.
This property is defined as the _inv -thd-waitq_(s) predicate as follows.

_inv -thd-waitq_ s  _$\equiv$_  _$($__$\forall\,$_ p _$\in$_ mem-pools s
_$\mathord{.}$_  _$\forall\,$_ t _$\in$_ set  _$($_ wait-q  _$($_ mem-pool-
info s p _$)$__$)$__$\mathord{.}$_ thd-state s t  _$=$_ BLOCKED _$)$_

_$\wedge$_  _$($__$\forall\,$_ t _$\mathord{.}$_ thd-state s t  _$=$_ BLOCKED
_$\longrightarrow$_  _$($__$\exists\,$_ p _$\in$_ mem-pools s _$\mathord{.}$_
t  _$\in$_ set  _$($_ wait-q  _$($_ mem-pool-info s p _$)$__$)$__$)$__$)$_

_$\wedge$_  _$($__$\forall\,$_ p _$\in$_ mem-pools s _$\mathord{.}$_ dist-list
_$($_ wait-q  _$($_ mem-pool-info s p _$)$__$)$__$)$_

_$\wedge$_  _$($__$\forall\,$_ p q _$\mathord{.}$_ p _$\in$_ mem-pools s
_$\wedge$_ q _$\in$_ mem-pools s  _$\wedge$_ p  _$\not=$_ q
_$\longrightarrow$_

_$($__$\nexists\,$_ t _$\mathord{.}$_ t  _$\in$_ set  _$($_ wait-q  _$($_ mem-
pool-info s p _$)$__$)$_  _$\wedge$_ t _$\in$_ set  _$($_ wait-q  _$($_ mem-
pool-info s q _$)$__$)$__$)$__$)$_

####  3.2.7. Consistency of freeing and allocating blocks

During allocation and release of a memory block, blocks of the tree may
temporally be manipulated during the coalesce and division process. A block
can be only manipulated by a thread at a time, and the state bit of a block
being temporally manipulate has to be _FREEING_ or _ALLOCATING_. Moreover, one
of these memory blocks is being manipulated at most by one thread. This
property is defined as the _inv -aux-vars_(s) predicate as follows.

_inv -aux-vars_ s  _$\equiv$_

_$($__$\forall\,$_ t n _$\mathord{.}$_ freeing-node s t  _$=$_ Some n
_$\longrightarrow$_ get-bit  _$($_ mem-pool-info s _$)$_  _$($_ pool n _$)$_
_$($_ level n _$)$_  _$($_ block n _$)$_  _$=$_ FREEING _$)$_ _$\wedge$_

_$($__$\forall\,$_ n _$\mathord{.}$_ get-bit  _$($_ mem-pool-info s _$)$_
_$($_ pool n _$)$_  _$($_ level n _$)$_  _$($_ block n _$)$_  _$=$_ FREEING
_$\wedge$_ mem-block-addr-valid s n  _$\longrightarrow$_

 _$($__$\exists\,$_ t _$\mathord{.}$_ freeing-node s t  _$=$_ Some n
_$)$__$)$_ _$\wedge$_

_$($__$\forall\,$_ t n _$\mathord{.}$_ allocating-node s t  _$=$_ Some n
_$\longrightarrow$_

get-bit  _$($_ mem-pool-info s _$)$_  _$($_ pool n _$)$_  _$($_ level n _$)$_
_$($_ block n _$)$_  _$=$_ ALLOCATING _$)$_ _$\wedge$_

_$($__$\forall\,$_ n _$\mathord{.}$_ get-bit  _$($_ mem-pool-info s _$)$_
_$($_ pool n _$)$_  _$($_ level n _$)$_  _$($_ block n _$)$_  _$=$_ ALLOCATING
_$\wedge$_ mem-block-addr-valid s n  _$\longrightarrow$_

 _$($__$\exists\,$_ t _$\mathord{.}$_ allocating-node s t  _$=$_ Some n
_$)$__$)$_ _$\wedge$_

_$($__$\forall\,$_ t1 t2 n1 n2 _$\mathord{.}$_ t1  _$\not=$_ t2  _$\wedge$_
freeing-node s t1  _$=$_ Some n1  _$\wedge$_ freeing-node s t2  _$=$_ Some n2
_$\longrightarrow$_

 _$\neg$__$($_ pool n1  _$=$_ pool n2  _$\wedge$_ level n1  _$=$_ level n2
_$\wedge$_ block n1  _$=$_ block n2 _$)$__$)$_ _$\wedge$_

_$($__$\forall\,$_ t1 t2 n1 n2 _$\mathord{.}$_ t1  _$\not=$_ t2  _$\wedge$_
allocating-node s t1  _$=$_ Some n1  _$\wedge$_ allocating-node s t2  _$=$_
Some n2  _$\longrightarrow$_

 _$\neg$__$($_ pool n1  _$=$_ pool n2  _$\wedge$_ level n1  _$=$_ level n2
_$\wedge$_ block n1  _$=$_ block n2 _$)$__$)$_ _$\wedge$_

_$($__$\forall\,$_ t1 t2 n1 n2 _$\mathord{.}$_ allocating-node s t1  _$=$_
Some n1  _$\wedge$_ freeing-node s t2  _$=$_ Some n2  _$\longrightarrow$_

 _$\neg$__$($_ pool n1  _$=$_ pool n2  _$\wedge$_ level n1  _$=$_ level n2
_$\wedge$_ block n1  _$=$_ block n2 _$)$__$)$_

###  3.3. Memory Separation

To operate securely, the memory management must enforce memory separation.
That is, it must prevent memory leaks and insecure data flows. Informally,
this means that it must prevent memory leaks among blocks due to incorrect
memory split and coalescing for the Zephir buddy memory allocation service. It
also must avoid that an allocated memory areas is influenced by any thread
different than the one carrying out the allocation of that area. We call the
two security properties memory separation at memory-block level and at thread
level respectively.

####  3.3.1. Memory Separation at Memory-block Level

When allocating and releasing memory for threads, the memory allocator must
correctly manage the allocated and freed memory blocks. On one hand, it should
prevent allocating one memory address to multiple memory blocks to avoid
possible data leaks among threads. On the other hand, it should be able to
control all the memory addresses in a memory pool to avoid interspaces between
memory blocks. Therefore, memory blocks in a memory pool partition its address
space, i.e. blocks are not overlapping each other and the addresses of all
blocks cover the address space of the pool.

For a memory block with index $j$ at level $i$, its address space is the
interval $[j\times(max\\_sz/4^{i}),(j+1)\times(max\\_sz/4^{i}))$. For any
relative memory address $addr$ in the memory domain of a memory pool, and
hence $addr<n\\_max*max\\_sz$, there is one and only one memory block whose
address space contains $addr$. Here, we use relative address for $addr$. The
property is defined as the _mem -part_(s) predicate as follows.

_addr -in-block_ mp addr i j  _$\equiv$_ i  _$ <$_ length  _$($_ levels mp
_$)$_  _$\wedge$_ j  _$ <$_ length  _$($_ bits  _$($_ levels mp  _$!$_ i
_$)$__$)$_ _$\wedge$_

_$($_ bits  _$($_ levels mp  _$!$_ i _$)$_  _$!$_ j  _$=$_ FREE  _$\vee$_ bits
_$($_ levels mp  _$!$_ i _$)$_  _$!$_ j  _$=$_ FREEING  _$\vee$_

bits  _$($_ levels mp  _$!$_ i _$)$_  _$!$_ j  _$=$_ ALLOCATED  _$\vee$_ bits
_$($_ levels mp  _$!$_ i _$)$_  _$!$_ j  _$=$_ ALLOCATING _$)$_ _$\wedge$_

addr  _$\in$_  _$\\{$_ j  _$*$_  _$($_ max-sz mp div  _$($_ 4 ^ i _$)$__$)$_
_$\mathord{.}$__$\mathord{.}$__$ <$_ (j+1)  _$*$_  _$($_ max-sz mp div  _$($_
4 ^ i _$)$__$)$__$\\}$_

_mem -part_ s  _$\equiv$_  _$\forall\,$_ p _$\in$_ mem-pools s _$\mathord{.}$_
let mp  _$=$_ mem-pool-info s p in

_$($__$\forall\,$_ addr  _$ <$_ n-max mp  _$*$_ max-sz mp _$\mathord{.}$_
_$($__$\exists\,$__$!$__$($_ i _$\mathord{,}$_ j _$)$__$\mathord{.}$_ addr-in-
block mp addr i j _$)$_  _$)$_

From the invariants of bitmaps and memory configuration in the previous
subsection, we can derive the general property for the memory partition as the
following theorem.

###### Theorem 3.1 (Memory Partition).

For any kernel state $s$, If the memory pools in $s$ are consistent in their
configuration, and their bitmaps are well-shaped, the memory pools satisfy the
partition property in $s$, i.e.

$\textbf{inv\\_mempool\\_info}(s)\wedge\textbf{inv\\_bitmap}(s)\wedge\textbf{inv\\_bitmap0}(s)\wedge\textbf{inv\\_bitmapn}(s)\Longrightarrow\textbf{mem\\_part}(s)$

That is, the proof for the memory separation preservation at the memory-block
level is discharged by the proof of the invariants preservation.

####  3.3.2. Memory Separation at Thread Level

When a thread requests for memory blocks, the memory management allocates some
block to that thread by adding it to the local memory of the thread. As a
consequence the thread becomes the exclusive owner of the block, which can
only be freed by the same thread that the block belongs to. For this purpose,
we define a mapping of allocated memory blocks of threads in the system state
of the memory management as

$mblocks::Thread\Rightarrow Mem\\_block\ set$

The execution of memory services by a thread $t$ cannot affect the allocated
memory blocks of other threads, i.e. for arbitrary states $s$ and $r$, which
are the previous state and the following state of an execution step of $t$
respectively, the memory separation requires that

$\forall t^{\prime}.t^{\prime}\neq t\longrightarrow mblocks\ s\
t^{\prime}=mblocks\ r\ t^{\prime}$

In Section 6.5, we will show that the separation property implies integrity of
the memory management services.

##  4\. Formalizing Zephyr Memory Management

In this section, we first introduce an execution model of Zephyr using the
PiCore language. Then we discuss in detail the low-level design specification
for the kernel services that the memory management provides. Since this work
focuses on the memory management, we only provide very abstract models for
other kernel functionalities such as the kernel scheduling and thread control.

###  4.1. Event-based Execution Model of Zephyr

####  4.1.1. PiCore statements for memory management

Interrupt handlers in OSs are considered as reaction services of PiCore
representing as _events_ :

$\textbf{EVENT}\ {\mathcal{E}}\ [{p_{1},...,p_{n}}]@{\kappa}\ \textbf{WHEN}\
{g}\ \textbf{THEN}\ {P}\ \textbf{END}$

In addition to the input parameters, an event has a special parameter $\kappa$
indicating the execution context, e.g. the scheduler and the thread invoking
the event. The imperative commands of an event body $P$ in PiCore are standard
sequential constructs such as conditional execution, loop, and sequential
composition of programs. It also includes a synchronization construct for
concurrent processes represented by $\textbf{AWAIT}\ {b}\ \textbf{THEN}\ {P}\
\textbf{END}$. The body $P$ is executed atomically if and only if the boolean
condition $b$ holds, not progressing otherwise. $\textbf{ATOM}\ {P}\
\textbf{END}$ denotes an _Await_ statement for which its guard is $True$.

Threads and kernel processes have their own execution context and local
states. Each of them is modelled in PiCore as a set of events called _event
systems_ and denoted as $\textbf{ESYS}\
{\mathcal{S}}\equiv\\{{\mathcal{E}_{0}},\ ...,\ {\mathcal{E}_{n}}\\}$. The
operational semantics of an event system is the _sequential composition_ of
the execution of the events composing it. Finally, PiCore has a construct for
parallel composition of event systems $esys_{0}\parallel...\parallel esys_{n}$
which interleaves the execution of the events composing each event system
$esys_{i}$ for $0\leq i\leq n$.

####  4.1.2. Execution model of Zephyr

Figure 8. An Execution Model of Zephyr Memory Management

After being initialized, an OS kernel can be considered as a reactive system
that is in an _idle_ loop until it receives an interruption which is handled
by an interruption handler. Whilst an interrupt handler execution is atomic in
sequential kernels, it can be interrupted in concurrent kernels (Chen et al.,
2016; Xu et al., 2016) allowing services invoked by threads to be interrupted
and resumed later. In the execution model of Zephyr, we consider a scheduler
$\mathcal{S}$, a timer and a set of threads $t_{1},...,t_{n}$. In this model,
the execution of the scheduler is atomic since kernel services can not
interrupt it. But kernel services can be interrupted via the scheduler, i.e.,
the execution of a memory service invoked by a thread $t_{i}$ may be
interrupted by the kernel scheduler to execute a thread $t_{j}$. Fig.8
illustrates Zephyr execution model, where solid lines represent execution
steps of the threads/kernel services and dotted lines mean the suspension of
the thread/code. For instance, the execution of _k_mempool_free_ in thread
$t_{1}$ is interrupted by the scheduler, and the context is switched to thread
$t_{2}$, which invokes _k_mempool_alloc_. During the execution of $t_{2}$, the
kernel service may suspend the thread and switch to another thread $t_{n}$ by
calling _rescheduling_. Later, the execution is switched back to $t_{1}$ and
continues the execution of _k_mempool_free_ in a different state from when it
was interrupted.

The event systems of Zephyr are illustrated in the right part of Fig. 8. A
user thread $t_{i}$ invoke allocation/release services, thus the event system
for $t_{i}$ is $esys_{t_{i}}$, a set composed of the events _alloc_ and
_free_. The input parameters for these events correspond with the arguments of
the service implementation, that are constrained by the guard for each
service. Together with system users we model the event service for the
scheduler $esys_{sched}$ consisting on a unique event _sched_ whose argument
is a thread $t$ to be scheduled when $t$ is in the _READY_ state. The formal
specification of the memory management is the parallel composition of the
event system for the threads, the scheduler and the timer.

####  4.1.3. Thread context and preemption

Events are parametrized by a thread identifier used to access to the execution
context of the thread invoking it. As shown in Figure 8, the execution of an
event executed by a thread can be stopped by the scheduler to be resumed
later. This behaviour is modelled using a global variable $cur$ indicating
that the thread being currently has been scheduled and it is being executed.
The model conditions the execution of parametrized events in $t$ only when $t$
is scheduled. This is achieved by using the expression t $\blacktriangleright$
p $\equiv$ $\textbf{AWAIT}\ {cur=t}\ \textbf{THEN}\ {p}\ \textbf{END}$, so an
event invoked by a thread $t$ only progresses when $t$ is scheduled. This
scheme allows to use rely-guarantee for concurrent execution of threads on
mono-core architectures, where only the scheduled thread is able to modify the
memory.

###  4.2. Formal Specification of Memory Management Services

This section discusses the formal specification of the memory management
services. These services deal with the initialization of pools, and memory
allocation and release.

####  4.2.1. System state

The system state includes the memory model introduced in Section 3, together
with the thread under execution represented by the variable $cur$ and the
local variables to the memory services. The local variables are used to keep
temporal changes to the structure, guards in conditional and loop statements,
and index accesses. The memory model is represented as a set _mem_pools_
storing the references of all memory pools and a mapping _mem_pool_info_ to
query a pool by a pool reference. Local variables are modelled as total
functions from threads to variable values, representing that the event is
accessing the thread context. In the formal model of the events we represent
the access to a state component $c$ with ${\emph{\'{\relax}}}c$ and the value
of a local component $c$ for the thread $t$ is represented as
${\emph{\'{\relax}}}c\ t$. Local variables _allocating_node_ and
_freeing_node_ are relevant for the memory services, storing the temporal
blocks being split/coalesced in alloc/release services respectively. The
memory blocks allocated in a thread are stored in the local variable _mblocks_
as discussed in the previous section.

####  4.2.2. Memory pool initialization

Zephyr defines and initializes memory pools at compile time by constructing a
static variable of type _struct k_mem_pool_. The implementation initializes
each pool with _n_max_ level 0 blocks with size _max_sz_ bytes. Bitmaps of
level 0 are set to 1 and free list contains all level 0 blocks. Bitmaps and
free lists of other level are initialized to 0 and to the empty list
respectively. In the formal model, we specify a state corresponding to the
implementation initial state and we show that it belongs to the set of states
satisfying the invariant.

####  4.2.3. Memory allocation/release services

The C code of Zephyr uses the recursive function _free_block_ to coalesce free
partner blocks and the _break_ statement to stop the execution of a loop
statements, which are not supported by the imperative language in PiCore. The
formal specification overcomes this by transforming the recursion into a loop
controlled by the recursion condition, and using a control variable to exit
loops with breaks when the condition to execute the loop break is satisfied.
Additionally, the memory management services use the atomic body _irq_lock();
P; irq_unlock();_ to keep interruption handlers _reentrant_ by disabling
interruptions. We simplify this behaviour in the specification using an ATOM
statement, avoiding the service to be interrupted at that point. The rest of
the formal specification closely follows the implementation, where variables
are modified using higher order functions changing the state as the code does
it. The reason of using Isabelle/HOL functions is that PiCore does not provide
a semantic for expressions, using instead state transformer relying on high
order functions to change the state.

1  _WHILE_  _´_ free-block-r t  _DO_

2 t $\blacktriangleright$  _´_ lsz  _$\mathord{:}$__$=$_  _´_ lsz  _$($_ t
_$\mathord{:}$__$=$_  _´_ lsizes t  _$!$_  _$($__´_ lvl t
_$)$__$)$__$\mathord{;}$__$\mathord{;}$_

3 t $\blacktriangleright$  _´_ blk  _$\mathord{:}$__$=$_  _´_ blk  _$($_ t
_$\mathord{:}$__$=$_ block-ptr  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$_  _$($__´_ lsz t _$)$_  _$($__´_ bn t
_$)$__$)$__$\mathord{;}$__$\mathord{;}$_

4 t $\blacktriangleright$  _ATOM_

5  _´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-free  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t
_$)$__$\mathord{;}$__$\mathord{;}$_

6  _´_ freeing-node  _$\mathord{:}$__$=$_  _´_ freeing-node  _$($_ t
_$\mathord{:}$__$=$_ None _$)$__$\mathord{;}$__$\mathord{;}$_

7  _IF_  _´_ lvl t  _$ >$_ 0  _$\wedge$_ partner-bits  _$($__´_ mem-pool-info
_$($_ pool b _$)$__$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t _$)$_  _THEN_

8  _FOR_  _´_ i  _$\mathord{:}$__$=$_  _´_ i _$($_ t  _$\mathord{:}$__$=$_ 0
_$)$__$\mathord{;}$_  _´_ i t  _$ <$_ 4 _$\mathord{;}$_  _´_ i
_$\mathord{:}$__$=$_  _´_ i _$($_ t  _$\mathord{:}$__$=$_  _´_ i t  _$+$_ 1
_$)$_  _DO_

9  _´_ bb  _$\mathord{:}$__$=$_  _´_ bb  _$($_ t  _$\mathord{:}$__$=$_
_$($__´_ bn t div 4 _$)$_  _$*$_ 4  _$+$_  _´_ i t
_$)$__$\mathord{;}$__$\mathord{;}$_

10  _´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-noexist  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bb t
_$)$__$\mathord{;}$__$\mathord{;}$_

11  _´_ block-pt  _$\mathord{:}$__$=$_  _´_ block-pt  _$($_ t
_$\mathord{:}$__$=$_ block-ptr  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$_  _$($__´_ lsz t _$)$_  _$($__´_ bb t
_$)$__$)$__$\mathord{;}$__$\mathord{;}$_

12  _IF_  _´_ bn t  _$\not=$_  _´_ bb t  _$\wedge$_ block-fits  _$($__´_ mem-
pool-info  _$($_ pool b _$)$__$)$_  _$($__´_ block-pt t _$)$_  _$($__´_ lsz t
_$)$_  _THEN_

13  _´_ mem-pool-info  _$\mathord{:}$__$=$_  _´_ mem-pool-info  _$($__$($_
pool b _$)$_  _$\mathord{:}$__$=$_

14 remove-free-list  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$($__´_
lvl t _$)$_  _$($__´_ block-pt t _$)$__$)$_

15  _FI_

16  _ROF_ _$\mathord{;}$__$\mathord{;}$_

17  _´_ lvl  _$\mathord{:}$__$=$_  _´_ lvl  _$($_ t  _$\mathord{:}$__$=$_  _´_
lvl t  _$-$_ 1 _$)$__$\mathord{;}$__$\mathord{;}$_

18  _´_ bn  _$\mathord{:}$__$=$_  _´_ bn  _$($_ t  _$\mathord{:}$__$=$_  _´_
bn t div 4 _$)$__$\mathord{;}$__$\mathord{;}$_

19  _´_ mem-pool-info  _$\mathord{:}$__$=$_ set-bit-freeing  _´_ mem-pool-info
_$($_ pool b _$)$_  _$($__´_ lvl t _$)$_  _$($__´_ bn t
_$)$__$\mathord{;}$__$\mathord{;}$_

20  _´_ freeing-node  _$\mathord{:}$__$=$_  _´_ freeing-node  _$($_ t
_$\mathord{:}$__$=$_ Some  _$\mathopen{(\mkern-3.0mu\mid}$_ pool  _$=$_  _$($_
pool b _$)$__$\mathord{,}$_ level  _$=$_  _$($__´_ lvl t _$)$__$\mathord{,}$_

21 block  _$=$_  _$($__´_ bn t _$)$__$\mathord{,}$_ data  _$=$_ block-ptr
_$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_

22 _$($__$($__$($_ ALIGN4  _$($_ max-sz  _$($__´_ mem-pool-info  _$($_ pool b
_$)$__$)$__$)$__$)$_ div  _$($_ 4 ^  _$($__´_ lvl t _$)$__$)$__$)$__$)$_
_$($__´_ bn t _$)$_  _$\mathclose{\mid\mkern-3.0mu)}$__$)$_

23  _ELSE_

24  _IF_ block-fits  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$($__´_
blk t _$)$_  _$($__´_ lsz t _$)$_  _THEN_

25  _´_ mem-pool-info  _$\mathord{:}$__$=$_  _´_ mem-pool-info  _$($__$($_
pool b _$)$_  _$\mathord{:}$__$=$_

26 append-free-list  _$($__´_ mem-pool-info  _$($_ pool b _$)$__$)$_  _$($__´_
lvl t _$)$_  _$($__´_ blk t _$)$_  _$)$_

27  _FI_ _$\mathord{;}$__$\mathord{;}$_

28  _´_ free-block-r  _$\mathord{:}$__$=$_  _´_ free-block-r  _$($_ t
_$\mathord{:}$__$=$_ False _$)$_

29  _FI_

30  _END_

31  _OD_

Figure 9. The PiCore Specification of _free_block_

Fig. 9 illustrates the PiCore specification of the _free_block_ function
invoked by _k_mem_pool_free_ when releasing a memory block. The code accesses
the following variables: $lsz$, $lsize$, and $lvl$ to keep information about
the current level; $blk$, $bn$, and $bb$ to represent the address and number
of the block currently being accessed; $freeing\\_node$ to represent the node
being freeing; and $i$ to iterate blocks. Additionally, the model includes the
component $free\\_block\\_r$ to model the recursion condition. To simplify the
representation the model uses predicates and functions to access and modify
the state. We refer readers to the Isabelle/HOL sources for the complete
specification of these functions and the complete formal model.

In the C code, _free_block_ is a recursive function with two conditions: (1)
the block being released belongs to a level higher than zero, since blocks at
level zero cannot be merged; and (2) the partners bits of the block being
released are FREE so they can be merged into a bigger block. We represent (1)
with the predicate ${\emph{\'{\relax}}}lvl\ t\ {\emph{$>$}}\ {0}$ and (2) with
the predicate $partner\\_bit\\_free$. The formal specification follows the
same structure translating the recursive function into a loop that is
controlled by a variable mimicking the recursion. The recursive process of
_free_block_ is illustrated in Fig. 10.

Figure 10. Coalescing Memory Blocks in _free_block_

The formal specification for _free_block_ first releases an allocated memory
block $bn$ setting it to _FREEING_. Then, the loop statement sets _free_block_
to _FREE_ (Line 5 in Fig. 9), and also checks that the iteration/recursive
condition holds in Line 7. If the condition holds, the partner bits are set to
_NOEXIST_ , and remove their addresses from the free list for this level
(Lines 12 - 15). Then, it sets the parent block bit to _FREEING_ (Lines 17 -
22), and updates the variables controlling the current block and level
numbers, before going back to the beginning of the loop again. If the
iteration condition is not true it sets the bit to _FREE_ and add the block to
the free list (Lines 24 - 28) and sets the loop condition to false to end the
procedure. This function is illustrated in Fig. 10. The block $174$ is
released by a thread and since its partner blocks (block $172$, $173$ and
$175$) are free, Zephyr coalesces the four blocks and sets their parent block
$43$ as _FREEING_. The coalescence continues iteratively if the partners of
block $43$ are all free.

The main part of the C code of the _k_mem_pool_free_ service and its complete
formalization are shown in Appendices A and B respectively.

####  4.2.4. Formal specification of the memory management

The PiCore specification of the memory management of Zephyr is finally defined
as follows. The events for the scheduler and the timer is simple. The
_schedule_ event chooses a _READY_ thread _t_ to be executing and set the
current thread to _READY_. The _tick_ event just increases the _tick_ variable
in system state by one. The _tick_ variable is used for the _time out_ waiting
mode for memory allocation.

(1) $\displaystyle Mem\\_Spec\equiv\lambda\kappa.\ \textbf{case}\ \kappa\
\textbf{of}$ $\displaystyle(\textbf{\emph{$\mathcal{T}$}}\ t)\
\emph{$\Rightarrow$}\ \bigcup{b}.\ \\{free(b)@t\\}\cup\bigcup{(p,sz,to)}.\
\\{alloc(p,sz,to)@t\\}$ $\displaystyle\emph{$\mid$}$
$\displaystyle\textbf{\emph{$\mathcal{S}$}}\ \emph{$\Rightarrow$}\
\bigcup{t}.\ \\{schedule(t)\\}$ $\displaystyle\emph{$\mid$}$
$\displaystyle\textbf{Timer}\ \emph{$\Rightarrow$}\ \\{tick\\}$

##  5\. Compositional Reasoning about Integrity in PiCore

In this section, we present a compositional reasoning approach for the
verification of integrity in PiCore. We use the notion of integrity from
(Rushby, 1992; Murray et al., 2012), which provides a formalism for the
specification of security policies. We first define the integrity of PiCore
specification. Then, we show that reasoning about the integrity of the system
can be decomposed to events. For convenience, we first introduce the
operational semantics and computations of PiCore in brief, which is the
foundation of the integrity and its compositional reasoning.

###  5.1. Operational Semantics and Computations of PiCore

The semantics of PiCore is defined via transition rules between
configurations. We define a configuration $\mathcal{C}$ in PiCore as a triple
$(\sharp,s,x)$ where $\sharp$ is a specification, $s:S$ is a system state, and
$x:\mathcal{K}\rightarrow\mathcal{E}$ is an event context. The event context
indicates which event is currently being executed in an event system $\kappa$.
$\sharp_{\mathcal{C}}$, $s_{\mathcal{C}}$, and $x_{\mathcal{C}}$ represent the
projection of each component in the tuple $\mathcal{C}=(\sharp,s,x)$.
Transition rules in events, event systems, and parallel event systems have the
form
$\Sigma\vdash(\sharp_{1},s_{1},x_{1})\stackrel{{\scriptstyle{\delta}}}{{\longrightarrow}}_{\square}(\sharp_{2},s_{2},x_{2})$,
where $\delta={t}@{\kappa}$ is a label indicating the type of transition, the
subscript “$\square$” (e, es or pes) indicates the transition objects, and
$\Sigma$ is used for some static configuration for programs (e.g. an
environment for procedure declarations). Here $t$ indicates a program action
$c$ or an occurrence of an event $\mathcal{E}$. $@\kappa$ means that the
action occurs in event system $\kappa$. Environment transition rules have the
form
$\Sigma\vdash(\sharp,s,x)\stackrel{{\scriptstyle{env}}}{{\longrightarrow}}_{\square}(\sharp,s^{\prime},x^{\prime})$.
Intuitively, a transition made by the environment may change the state but not
the event context nor the specification. The parallel composition of event
systems is fine-grained since small steps in events are interleaved in the
semantics of PiCore.

A _computation_ of PiCore is a sequence of transitions. We define the set of
computations of all parallel event systems with static information $\Sigma$ as
$\Psi(\Sigma)$, which is a set of lists of configurations inductively defined
as follows. The singleton list is always a computation (1). Two consecutive
configurations are part of a computation if they are the initial and final
configurations of an environment (2) or action transition (3).

$\footnotesize\left\\{\begin{aligned}
&(1)[(\mathcal{PS},s,x)]\in\Psi(\Sigma)\\\
&(2)(\mathcal{PS},s_{1},x_{1})\\#cs\in\Psi(\Sigma)\Longrightarrow(\mathcal{PS},s_{2},x_{2})\\#(\mathcal{PS},s_{1},x_{1})\\#cs\in\Psi(\Sigma)\\\
&(3)\Sigma\vdash(\mathcal{PS}_{2},s_{2},x_{2})\stackrel{{\scriptstyle{\delta}}}{{\longrightarrow}}_{pes}(\mathcal{PS}_{1},s_{1},x_{1})\wedge(\mathcal{PS}_{1},s_{1},x_{1})\\#cs\in\Psi(\Sigma)\\\
&\quad\quad\quad\Longrightarrow(\mathcal{PS}_{2},s_{2},x_{2})\\#(\mathcal{PS}_{1},s_{1},x_{1})\\#cs\in\Psi(\Sigma)\end{aligned}\right.$

Computations for events and event systems are defined in a similar way. We use
$\Psi(\Sigma,\mathcal{PS})$ to denote the set of computations of a parallel
event system $\mathcal{PS}$. The function $\Psi(\Sigma,\mathcal{PS},s,x)$
denotes the computations of $\mathcal{PS}$ starting up from an initial state
$s$ and event context $x$.

In PiCore, the semantics is compositional. A computation $\varpi$ of
$\mathcal{PS}$ could be decomposed into a set of computations $\tilde{\varpi}$
of its event systems. Computations in $\tilde{\varpi}$ have the same state and
event context sequence. They do not have component transitions at the same
time. $\varpi$ also has the same state and event context sequence as
$\tilde{\varpi}$. Furthermore, in $\varpi$ a transition is labelled as
$\delta$ if this is the label in one of the computations $\tilde{\varpi}$ at
the corresponding position; a transition is an environment transition if this
is the case in all computations $\tilde{\varpi}$ at the corresponding
position. We use the _conjoin_ notation $\varpi\ \emph{$\propto$}\
\tilde{\varpi}$ to present this compositionality, and
$\tilde{\varpi}^{\kappa}$ denotes the computation of $\kappa$.

###  5.2. Integrity in PiCore

In general, the definition of integrity relies on a security configuration for
a system, which is actually the security policies, as well as a state machine
of the system.

####  5.2.1. Security Configuration

In order to discuss the security of a PiCore specification $\mathcal{PS}$, we
assume a set of security domains $\mathcal{D}$ and a security policy
$\leadsto$ that restricts the allowable flow of information among those
domains. The security policy $\leadsto$ is a reflexive relation on
$\mathcal{D}$. $d_{1}\leadsto d_{2}$ means that actions performed by $d_{1}$
can influence subsequent outputs seen by $d_{2}$.
$\mathrel{\mathchoice{{\ooalign{$\displaystyle/$\cr\hfil$\displaystyle\leadsto$\hfil\cr}}}{{\ooalign{$\textstyle/$\cr\hfil$\textstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptstyle/$\cr\hfil$\scriptstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle/$\cr\hfil$\scriptscriptstyle\leadsto$\hfil\cr}}}}$
is the complement relation of $\leadsto$. We call $\leadsto$ and
$\mathrel{\mathchoice{{\ooalign{$\displaystyle/$\cr\hfil$\displaystyle\leadsto$\hfil\cr}}}{{\ooalign{$\textstyle/$\cr\hfil$\textstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptstyle/$\cr\hfil$\scriptstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle/$\cr\hfil$\scriptscriptstyle\leadsto$\hfil\cr}}}}$
the _interference_ and _noninterference_ relations respectively.

Each event has associated an execution domain responsible of invoking the
event. Traditional formulations in information-flow security assume a static
mapping from events to domains, such that the domain of an event can be
determined solely from the event itself (Rushby, 1992; von Oheimb, 2004). For
flexibility, we use a dynamic mapping, which is represented by a function
$dom\\_e:S\times\mathcal{K}\times\mathcal{E}\rightarrow\mathcal{D}$, and
$dom\\_e(s,\kappa,ev)$ means the execution domain of event $ev$ on context
$\kappa$ in state $s$. The $\mathcal{PS}$ is _view-partitioned_ if, for each
domain $d\in\mathcal{D}$, there is an equivalent relation
$\stackrel{{\scriptstyle{d}}}{{\sim}}$ on $S$. For convenience, we define
$\mathcal{C}_{1}\stackrel{{\scriptstyle{d}}}{{\sim}}\mathcal{C}_{2}\triangleq
s_{\mathcal{C}_{1}}\stackrel{{\scriptstyle{d}}}{{\sim}}s_{\mathcal{C}_{2}}$.

####  5.2.2. State Machine Representation of PiCore Specification

The state-event IFS is usually defined on a state machine. Here, we construct
an equivalent state machine for a PiCore specification. The state of the
machine is the configuration in the PiCore semantics. The security of PiCore
consider small-step actions of systems. A small-step action in the machine is
identified by the label of a transition, the event that the action belongs to,
and the domain that triggers the event. A small-step action is thus in the
form of a triple $(\delta,ev,d)$. The label of the transition can represent an
occurrence of an event $ev_{a}$, or $c$ when is an internal step of an event
already triggered. In that case $x_{\mathcal{C}}(\kappa)$ stores the event
that is being executed. We construct a nondeterministic state machine for a
closed PiCore specification as follows. Here, a closed specification means
that we dont consider the environment of the whole system, i.e. the rely
condition of the system is the identity relation.

###### Definition 5.1.

A state machine of a specification $\mathcal{PS}$ is a quadruple
$\mathcal{M}=\langle\Delta,A,step,\mathcal{C}_{0}\rangle$, where

  * •

$\Delta$ is the set of configurations.

  * •

$A$ is the set of actions. An action is a triple
$a=\langle\delta,ev,d\rangle$, where $\delta$ is a transition label in the
PiCore semantics, $ev$ is an event, and $d$ is a domain. The notations
$\delta_{a}$, $ev_{a}$ and $d_{a}$ respectively denote the projections of the
components of an action $a$.

  * •

$step:A\rightarrow\mathbb{P}(\Delta\times\Delta)$ is the transition function,
where
$step(a)=\\{(\mathcal{C},\mathcal{C}^{\prime})\mid\Sigma\vdash\mathcal{C}\stackrel{{\scriptstyle{\delta_{a}}}}{{\longrightarrow}}_{pes}\mathcal{C}^{\prime}\wedge((\delta_{a}={ev_{a}}@{\kappa}\wedge
dom\\_e(s_{\mathcal{C}},\kappa,ev_{a})=d_{a})\vee(\delta_{a}={c}@{\kappa}\wedge
ev_{a}=x_{\mathcal{C}}(\kappa)\wedge
dom\\_e(s_{\mathcal{C}},\kappa,ev_{a})=d_{a}))\\}$.

  * •

$\mathcal{C}_{0}$ is the initial configuration $(\sharp_{0},s_{0},x_{0})$.

Based on the function $step$, we define the function $run$ as follows to
represent the execution of a sequence of actions.

$\left\\{\begin{aligned} &run(Nil)=Id\\\ &run(a\\#as)=step(a)\circ
run(as)\end{aligned}\right.$

We prove the following lemma to ensure that the state machine is an equivalent
representation of the PiCore specification.

###### Lemma 5.2 (Equivalence of PiCore and Its State Machine Representation).

The state machine defined in Definition 5.1 is an equivalent representation of
PiCore, i.e.,

  * •

If $(\mathcal{C}_{1},\mathcal{C}_{2})\in run(as)$, then $\exists\varpi.\
\varpi\in\Psi(\Sigma,\mathcal{PS})\wedge\varpi_{0}=\mathcal{C}_{1}\wedge
last(\varpi)=\mathcal{C}_{2}\wedge(\forall j<len(\varpi)-1.\
\Sigma\vdash\varpi_{j}\stackrel{{\scriptstyle{\delta_{as_{j}}}}}{{\longrightarrow}}_{pes}\varpi_{(j+1)})$,
and

  * •

If $\varpi\in\Psi(\Sigma,\mathcal{PS})\wedge\varpi_{0}=\mathcal{C}_{1}\wedge
last(\varpi)=\mathcal{C}_{2}\wedge(\forall j<len(\varpi)-1.\
\neg(\Sigma\vdash\varpi_{j}\stackrel{{\scriptstyle
env}}{{\longrightarrow}}_{pes}\varpi_{(j+1)}))$, then $\exists as.\
(\mathcal{C}_{1},\mathcal{C}_{2})\in run(as)\wedge(\forall j<len(\varpi)-1.\
\Sigma\vdash\varpi_{j}\stackrel{{\scriptstyle{\delta_{as_{j}}}}}{{\longrightarrow}}_{pes}\varpi_{(j+1)})$

where $\Psi(\Sigma,\mathcal{PS})$ is the set of computations of a parallel
event system $\mathcal{PS}$.

We consider closed specifications where there is no environment transition in
the computations of $\mathcal{PS}$, i.e., $\forall j<len(\varpi)-1.\
\neg(\Sigma\vdash\varpi_{j}\stackrel{{\scriptstyle
env}}{{\longrightarrow}}_{pes}\varpi_{(j+1)})$.

####  5.2.3. Integrity

Following the definitions of integrity in (Rushby, 1992; Murray et al., 2012),
we define an intuitive integrity property in PiCore as follows, which concerns
the small-step execution of the system.

###### Definition 5.3 (Integrity).

Integrity of a parallel event system $\mathcal{PS}$ with a static
configuration $\Sigma$ from the initial state $s_{0}$ and $x_{0}$ is defined
as

$\forall a,d,\mathcal{C},\mathcal{C}^{\prime}.\ \mathcal{R}(\mathcal{C})\wedge
d_{a}\mathrel{\mathchoice{{\ooalign{$\displaystyle/$\cr\hfil$\displaystyle\leadsto$\hfil\cr}}}{{\ooalign{$\textstyle/$\cr\hfil$\textstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptstyle/$\cr\hfil$\scriptstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle/$\cr\hfil$\scriptscriptstyle\leadsto$\hfil\cr}}}}d\wedge(\mathcal{C},\mathcal{C}^{\prime})\in
step(a)\longrightarrow\mathcal{C}\stackrel{{\scriptstyle{d}}}{{\sim}}\mathcal{C}^{\prime}$

where $\mathcal{R}(\mathcal{C})\equiv\exists as.\
(\mathcal{C}_{0},\mathcal{C})\in run(as)$ is a function to show that
configuration $\mathcal{C}$ is reachable from the initial configuration of the
system $\mathcal{C}_{0}$.

The intuition of integrity is that a small-step action $a$ executed in a
configuration $\mathcal{C}$ can only affect those domains for which the domain
executing $a$ is allowed to send information.

###  5.3. Compositional Reasoning

In order to decompose the integrity reasoning of the system to its events, we
define a form of integrity on event as follows.

###### Definition 5.4 (Integrity on Events).

The integrity on the events composing a parallel event system $\mathcal{PS}$
is defined as

$\forall ev\ d\ s\ s^{\prime}\ \kappa.\ ev\in
evts(\mathcal{PS})\wedge(s,s^{\prime})\in
G_{\Gamma(ev)}\wedge(dom\\_e(s,\kappa,ev)\mathrel{\mathchoice{{\ooalign{$\displaystyle/$\cr\hfil$\displaystyle\leadsto$\hfil\cr}}}{{\ooalign{$\textstyle/$\cr\hfil$\textstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptstyle/$\cr\hfil$\scriptstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle/$\cr\hfil$\scriptscriptstyle\leadsto$\hfil\cr}}}}d)\longrightarrow
s\stackrel{{\scriptstyle{d}}}{{\sim}}s^{\prime}$

where the $evts(\mathcal{PS})$ function returns all the events defined in a
specification $\mathcal{PS}$. We assume a function
$\Gamma:evts(\mathcal{PS})\rightarrow RGCond$, where $RGCond$ is the type of
the rely-guarantee specification, to specify the rely-guarantee specification
of events in $\mathcal{PS}$. $G_{\Gamma(ev)}$ is the guarantee condition in
the rely-guarantee specification of an event $ev$.

The integrity on events requires that when an event $ev$ is executed, the
interaction of $ev$ with the environment affects only those domains for which
the domain executing $ev$ is allowed to send information to, according to the
relation $\leadsto$. Different from the integrity on actions of parallel in
Definition 5.3, the integrity here considers the global effects of events to
the environment.

Next, we show the compositionality of integrity, i.e. the integrity on events
implies the integrity on parallel event systems. First, Lemma 5.5 shows the
consistency of the event context in computations under a closed
$\mathcal{PS}$, i.e., program transitions of $\mathcal{PS}$,
$\Sigma\vdash\varpi_{i}\stackrel{{\scriptstyle{{c}@{\kappa}}}}{{\longrightarrow}}_{pes}\varpi_{i+1}$,
should be a transition of the event currently being under execution.

###### Lemma 5.5.

For any closed $\mathcal{PS}$, if $\forall ev\in evts(\mathcal{PS}).\
is\\_basic(ev)$, that is, all events in $\mathcal{PS}$ are basic events, then
for any computation $\varpi$ of $\mathcal{PS}$, we have

$\forall i<len(\varpi)-1,\kappa.\
(\Sigma\vdash\varpi_{i}\stackrel{{\scriptstyle{{c}@{\kappa}}}}{{\longrightarrow}}_{pes}\varpi_{i+1})\longrightarrow(\exists
ev\in evts(\mathcal{PS}).\ x_{\varpi_{i}}(\kappa)=ev)$

###### Proof.

For the computation $\varpi$, we have its conjoined computations
$\tilde{\varpi}$ such that $\varpi\ \emph{$\propto$}\ \tilde{\varpi}$. Hence,
for a program transition
$\Sigma\vdash\varpi_{i}\stackrel{{\scriptstyle{{c}@{\kappa}}}}{{\longrightarrow}}_{pes}\varpi_{i+1}$,
we have that
$\Sigma\vdash\tilde{\varpi}_{i}^{\kappa}\stackrel{{\scriptstyle{c}@{\kappa}}}{{\longrightarrow}}_{es}\tilde{\varpi}_{i+1}^{\kappa}$.
Since, all events in $\mathcal{PS}$ are basic events, all events in the event
system $\mathcal{PS}(\kappa)$ are basic events too. Thus, there must be an
event occurrence transition
$\Sigma\vdash\tilde{\varpi}_{m}^{\kappa}\stackrel{{\scriptstyle{ev}@{\kappa}}}{{\longrightarrow}}_{es}\Sigma\vdash\tilde{\varpi}_{m+1}^{\kappa}$
where $m<i$ and $ev\in evts(\mathcal{PS})$. The transition sets the event
context of $\kappa$ to $ev$, and all transitions between $m$ and $i$ are
program transitions or environment transitions which will not change the event
context. ∎

Second, Lemma 5.6 shows the compositionality of guarantee conditions of events
in a valid and closed parallel event system, i.e., any component transition
must preserve the guarantee condition of the current event.

###### Lemma 5.6.

For any closed $\mathcal{PS}$, if

  1. (1)

$\mathcal{C}_{0}=(\mathcal{PS},s_{0},x_{0})$.

  2. (2)

events in $\mathcal{PS}$ are basic events, i.e., $\forall ev\in
evts(\mathcal{PS}).\ is\\_basic(ev)$.

  3. (3)

events in $\mathcal{PS}$ satisfy their rely-guarantee specification, i.e.,
$\forall ev\in evts(\mathcal{PS}).\ \Sigma\vdash{ev}\ \mathbf{sat}\
{\Gamma(ev)}$.

  4. (4)

from (3) we have $\Sigma\vdash{\mathcal{PS}}\ \mathbf{sat}\
{\langle\\{s_{0}\\},\\{\\},UNIV,UNIV\rangle}$.

then for any computation $\varpi\in\Psi(\mathcal{PS},s_{0},x_{0})$, we have

$\forall i<len(\varpi)-1,\kappa.\
(\Sigma\vdash\varpi_{i}\stackrel{{\scriptstyle{{c}@{\kappa}}}}{{\longrightarrow}}_{pes}\varpi_{i+1})\longrightarrow(s_{\varpi_{i}},s_{\varpi_{i+1}})\in
G_{\Gamma(x_{\varpi_{i}}(\kappa))}$

###### Proof.

From assumption (4), we know that the rely-guarantee specifications of each
event in assumption (3) are compositional, i.e. the execution of each event in
all computations of $\Psi(\mathcal{PS},s_{0},x_{0})$ preserves its
specification. For the computation $\varpi$, we have its conjoined
computations $\tilde{\varpi}$ such that $\varpi\ \emph{$\propto$}\
\tilde{\varpi}$. Hence, for a program transition
$\Sigma\vdash\varpi_{i}\stackrel{{\scriptstyle{{c}@{\kappa}}}}{{\longrightarrow}}_{pes}\varpi_{i+1}$,
we have that
$\Sigma\vdash\tilde{\varpi}_{i}^{\kappa}\stackrel{{\scriptstyle{c}@{\kappa}}}{{\longrightarrow}}_{es}\tilde{\varpi}_{i+1}^{\kappa}$.
Next, we apply induction on $\sharp_{\tilde{\varpi}_{0}^{\kappa}}$:

  1. (1)

$\sharp_{\tilde{\varpi}_{0}^{\kappa}}=\\{{\mathcal{E}_{0}},\ ...,\
{\mathcal{E}_{n}}\\}$: the execution of an event system is a sequence of
executions of its composed events. Thus, the program transition is a
transition of its one event. We split the computation
$\tilde{\varpi}^{\kappa}$ to a set of computations of events, and the program
transition is in a computation of an event $ev\in\\{{\mathcal{E}_{0}},\ ...,\
{\mathcal{E}_{n}}\\}$. By Lemma 5.5 and $\Sigma\vdash{ev}\ \mathbf{sat}\
{\Gamma(ev)}$, we have the conclusion.

  2. (2)

$\sharp_{\tilde{\varpi}_{0}^{\kappa}}={ev}\triangleright{\mathcal{S}}$: first,
if the transition is of the execution of $ev$, we have
$x_{\tilde{\varpi}_{i}^{\kappa}}(\kappa)=ev$ by Lemma 5.5 and the semantics of
event occurrence. Moreover, the execution of ${ev}\triangleright{\mathcal{S}}$
before position $i$ is the same as of $ev$ and $\Sigma\vdash{ev}\
\mathbf{sat}\ {\Gamma(ev)}$. We have $(s_{\varpi_{i}},s_{\varpi_{i+1}})\in
G_{\Gamma(x_{\varpi_{i}}(\kappa))}$. Second, if the transition is of the
execution of $\mathcal{S}$, we have the conclusion by the inductive case (1).

∎

By these two lemmas and the equivalence in Lemma 5.2, we have the following
theorem for the compositionality of integrity.

###### Theorem 5.7 (Compositionality of Integrity).

For a closed parallel event system $\mathcal{PS}$, if

  1. (1)

$\mathcal{C}_{0}=(\mathcal{PS},s_{0},x_{0})$.

  2. (2)

events in $\mathcal{PS}$ are basic events, i.e., $\forall ev\in
evts(\mathcal{PS}).\ is\\_basic(ev)$.

  3. (3)

events in $\mathcal{PS}$ satisfy their rely-guarantee specification, i.e.,
$\forall ev\in evts(\mathcal{PS}).\ \Sigma\vdash{ev}\ \mathbf{sat}\
{\Gamma(ev)}$.

  4. (4)

$\Sigma\vdash{\mathcal{PS}}\ \mathbf{sat}\
{\langle\\{s_{0}\\},\\{\\},UNIV,UNIV\rangle}$.

  5. (5)

$\mathcal{PS}$ satisfies the integrity on its events.

then $\mathcal{PS}$ preserves the integrity property.

We require that all events in $\mathcal{PS}$ are basic events to ensure the
event context in computations of $\mathcal{PS}$ is consistent before the
execution of an event. It is a reasonable assumption since anonymous events
are only used to represent intermediate specifications during the execution of
events and they do not change modify the event context. The assumption (4) is
to ensure the compositionality of the rely-guarantee specifications of each
event in assumption (3), i.e. the execution of each event in all computations
of $\Psi(\mathcal{PS},s_{0},x_{0})$ preserves its specification. It is a
highly relaxed condition and it is easy to prove. First, we only consider
closed concurrent systems starting from the initial state $s_{0}$. Thus, the
pre-condition only has the initial state and the rely condition is empty.
Second, we do not constrain the behaviour of the parallel event system, thus
the guarantee condition is the universal set. Third, the integrity only
concerns the action transition, but not the final state. Thus, the post-
condition is the universal set.

##  6\. Rely-guarantee Proof of Zephyr

We have proven correctness of the buddy memory management in Zephyr using the
rely-guarantee proof system of PiCore. We ensure functional correctness of
each kernel service w.r.t. the defined pre/post conditions, termination of
loop statements in the kernel services, the separation of local variables of
threads, safety by invariant preservation, and security by memory separation.
In this section, we introduce how these properties are specified and verified
using the PiCore rely-guarantee proof system.

Actually, the safety and security properties verified in this article can be
embedded in the guarantee conditions of events of the memory management
specification. In this section, we first present the rely-guarantee
specification of events.

###  6.1. Correctness of the Specification

Using the compositional reasoning of PiCore, correctness of Zephyr memory
management can be specified and verified with the rely-guarantee specification
of each event.

The guarantee conditions for both memory services are the same, which is
defined as:

_Mem -pool-guar_ t  _$\equiv$_ $\overbrace{Id}^{(1)}$  _$\cup$_  _$($_
$\overbrace{gvars\\_conf\\_stable}^{(2)}$ _$\cap$_

_$\\{$__$($_ s _$\mathord{,}$_ r _$)$__$\mathord{.}$_  _$($_ $\overbrace{cur\
s\ {\emph{$\not=$}}\ Some\ t\ {\emph{$\longrightarrow$}}\
gvars{\mbox{-}}nochange\ s\ r\ {\emph{$\wedge$}}\ lvars{\mbox{-}}nochange\ t\
s\ r}^{(3.1)}$ _$)$_

_$\wedge$_  _$($_ $\overbrace{cur\ s\ {\emph{$=$}}\ Some\ t\
{\emph{$\longrightarrow$}}\ inv\ s\ {\emph{$\longrightarrow$}}\ inv\
r}^{(3.2)}$ _$)$_  _$\wedge$_  _$($_
$\overbrace{{\emph{$\forall\,$}}t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}{\emph{$\mathord{.}$}}\ t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}\ {\emph{$\not=$}}\ t\
{\emph{$\longrightarrow$}}\ lvars{\mbox{-}}nochange\ t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}\ s\ r}^{(4)}$ _$)$_

_$\wedge$_  _$($_ $\overbrace{{\emph{$\forall\,$}}t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}{\emph{$\mathord{.}$}}\ t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}\ {\emph{$\not=$}}\ t\
{\emph{$\longrightarrow$}}\ mblocks\ s\ t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}=mblocks\ r\ t{\emph{$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$}}}^{(5)}$ _$)$__$\\}$_ _$\cap$_
$\overbrace{{\emph{$\mathopen{\\{\mkern-4.5mu\mid}$}}{\emph{\textordmasculine}}tick\
{\emph{$=$}}\
{\emph{\textordfeminine}}tick{\emph{$\mathclose{\mid\mkern-4.5mu\\}}$}}{\emph{$)$}}}^{(6)}$

This relation states that _alloc_ and _free_ services may not change the state
(1), e.g., a blocked await or selecting branch on a conditional statement. If
it changes the state then: (2) the static configuration of memory pools in the
model do not change; (3.1) if the scheduled thread is not the thread invoking
the event then variables for that thread do not change (since it is blocked in
an _Await_ as explained in Section 4); (3.2) if it is, then the relation
preserves the memory invariant, and consequently each step of the event needs
to preserve the invariant, where $inv$ is the conjunction of all invariant
properties defined in Section 3.2; (4) a thread does not change the local
variables of other threads; (5) it is the memory separation property at the
thread level, which means that a thread does not change the allocated memory
blocks of other threads; and (6) threads do not change the _tick_ of the
timer. Here,
${\emph{$\mathopen{\\{\mkern-4.5mu\mid}$}}{\emph{\textordmasculine}}tick\
{\emph{$=$}}\
{\emph{\textordfeminine}}tick{\emph{$\mathclose{\mid\mkern-4.5mu\\}}$}}$
defines a set of state pairs, where operator ${\emph{\textordmasculine}}tick$
represents the $tick$ field in the first state of a pair and
${\emph{\textordfeminine}}tick$ in the second state. It is equivalent to
$\\{(s,t).\ tick\ s=tick\ t\\}$.

We could find that the preservation of the memory configuration during small
steps of kernel services is represented as condition (2), the invariant
preservation as condition (3.2), the separation of local variables of threads
as condition (4), and the memory separation as condition (5).

The rely conditions for the both memory services are the same, which is
defined as:

_Mem -pool-rely_ t  _$\equiv$_ Id  _$\cup$_  _$($_ gvars-conf-stable _$\cap$_
_$\\{$__$($_ s _$\mathord{,}$_ r _$)$__$\mathord{.}$_ (inv s
_$\longrightarrow$_ inv r) _$\wedge$_ lvars-nochange t s r

_$\wedge$_ _$($_ cur s  _$=$_ Some t  _$\longrightarrow$_ mem-pool-info s
_$=$_ mem-pool-info r _$\wedge$_  _$($__$\forall\,$_ t _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$__$\mathord{.}$_ t _$\mskip
2.0mu{{}^{\prime}}\mskip-2.0mu$_  _$\not=$_ t  _$\longrightarrow$_ lvars-
nochange t _$\mskip 2.0mu{{}^{\prime}}\mskip-2.0mu$_ s r _$)$__$)$_

_$\wedge$_ mblocks s t = mblocks r t _$\\}$__$)$_

This relation states that the _alloc_ and _free_ services assume that the
environment does not change the state (_Id_), otherwise (1) the environment
does not change the static configuration of memory pools; (2) the environment
preserves the invariant; (3) the environment does not change the local
variables of thread $t$; (4) if the scheduled thread is the thread invoking
the event then memory is not changed and local variables of other threads are
not changed; and (5) the environment does not change the allocated memory
blocks of thread $t$.

The functional correctness is specified as the pre/post-conditions. For
instance, we prove that when starting in a valid memory configuration given by
the invariant, then if the allocation service does not returns an error code
then it returns a valid memory block with size bigger or equal than the
requested capacity. The property is specified by the following postcondition
of the allocation service:

_Mem -pool-alloc-pre_ t  _$\equiv$_  _$\\{$_ s _$\mathord{.}$_ inv s
_$\wedge$_ allocating-node s t  _$=$_ None  _$\wedge$_ freeing-node s t  _$=$_
None _$\\}$_

_Mem -pool-alloc-post_ t p sz timeout  _$\equiv$_

 _$\\{$_ s _$\mathord{.}$_ inv s  _$\wedge$_ allocating-node s t  _$=$_ None
_$\wedge$_ freeing-node s t  _$=$_ None

_$\wedge$_  _$($_ timeout  _$=$_ FOREVER  _$\longrightarrow$_

_$($_ ret s t  _$=$_ ESIZEERR  _$\wedge$_ mempoolalloc-ret s t  _$=$_ None
_$\vee$_

ret s t  _$=$_ OK  _$\wedge$_  _$($__$\exists\,$_ mblk _$\mathord{.}$_
mempoolalloc-ret s t  _$=$_ Some mblk  _$\wedge$_ mblk-valid s p sz mblk
_$)$__$)$__$)$_

_$\wedge$_  _$($_ timeout  _$=$_ NOWAIT  _$\longrightarrow$_

_$($__$($_ ret s t  _$=$_ ENOMEM  _$\vee$_ ret s t  _$=$_ ESIZEERR _$)$_
_$\wedge$_ mempoolalloc-ret s t  _$=$_ None _$)$_ _$\vee$_

_$($_ ret s t  _$=$_ OK  _$\wedge$_  _$($__$\exists\,$_ mblk _$\mathord{.}$_
mempoolalloc-ret s t  _$=$_ Some mblk  _$\wedge$_ mblk-valid s p sz mblk
_$)$__$)$__$)$_

_$\wedge$_  _$($_ timeout  _$ >$_ 0  _$\longrightarrow$_

_$($__$($_ ret s t  _$=$_ ETIMEOUT  _$\vee$_ ret s t  _$=$_ ESIZEERR _$)$_
_$\wedge$_ mempoolalloc-ret s t  _$=$_ None _$)$_ _$\vee$_

_$($_ ret s t  _$=$_ OK  _$\wedge$_  _$($__$\exists\,$_ mblk _$\mathord{.}$_
mempoolalloc-ret s t  _$=$_ Some mblk  _$\wedge$_ mblk-valid s p sz mblk
_$)$__$)$__$)$__$\\}$_

If a thread requests a memory block in mode _FOREVER_ , it may successfully
allocate a valid memory block, or fail (_ESIZEERR_) if the request size is
larger than the size of the memory pool. If the thread is requesting a memory
pool in mode _NOWAIT_ , it may also get _ENOMEM_ as a result if there is no
available blocks. But if the thread is requesting in mode _TIMEOUT_ , it will
get the result of _ETIMEOUT_ if there is no available blocks in _timeout_
milliseconds.

The property is indeed weak since even if the memory has a block able to
allocate the requested size before invoking the allocation service, another
thread running concurrently may have taken the block first during the
execution of the service. For the same reason, the released block may be taken
by another concurrent thread before the end of the release services.

###  6.2. Proof of Partial Correctness

In the PiCore system, verification of a rely-guarantee specification is
carried out by inductively applying the proof rules for each system event and
discharging the proof obligations the rules generate. Typically, these proof
obligations require to prove stability of the pre- and post-condition to check
that changes of the environment preserve them, and to show that a statement
modifying a state from the precondition gets a state belonging to the
postcondition.

The final theorem of functional correctness is as follows.

###### Theorem 6.1 (Functional Correctness of Memory Management).

$\Sigma\vdash{Mem\\_Spec}\ \mathbf{sat}\
{\langle\\{s_{0}\\},\\{\\},Guar,UNIV\rangle}$

where $Guar=tick\\_guar\ \cup\ schedule\\_guar\ \cup\ (\bigcup{t}.\
Mem\\_pool\\_guar\ t)$.

We consider that the memory management is a closed system, i.e., the
environment is the empty set. In the initial state $s_{0}$, we assume that (1)
the memory blocks at level 0 of all memory pools are free and not split, (2)
the current thread is None, (3) the state of all threads are _READY_ , and (4)
the wait queue of thread of each memory pool is empty. We have that $s_{0}$
satisfies the invariants.

By the Par rule in Fig. 6, the proof of Theorem 6.1 can be decomposed to the
satisfiability for each event of the proof of correctness of the specification
introduced in section 6.1. We proved the following lemmas for the memory
services. A detailed proof sketch and intermediate conditions of Lemma 6.3 is
shown in Appendix B.

###### Lemma 6.2 (Functional Correctness of the Allocation Service).

$\displaystyle\Sigma\vdash Mem\\_pool\\_alloc\ t\ p\ sz\ to\ \mathbf{sat}\
\langle$ $\displaystyle Mem\\_pool\\_alloc\\_pre\ t,Mem\\_pool\\_rely\ t,$
$\displaystyle Mem\\_pool\\_guar\ t,Mem\\_pool\\_alloc\\_post\ t\ p\ sz\
to\rangle$

###### Lemma 6.3 (Functional Correctness of the Release Service).

$\displaystyle\Sigma\vdash Mem\\_pool\\_free\ t\ p\ sz\ to\ \mathbf{sat}\
\langle$ $\displaystyle Mem\\_pool\\_free\\_pre\ t,Mem\\_pool\\_rely\ t,$
$\displaystyle Mem\\_pool\\_guar\ t,Mem\\_pool\\_free\\_post\ t\ p\ sz\
to\rangle$

###  6.3. Proof of Termination

To prove loop termination, loop invariants are parametrized with a logical
variable $\alpha$. It suffices to show total correctness of a loop statement
by the following proposition where $loopinv(\alpha)$ is the parametrize
invariant, in which the logical variable is used to find a convergent relation
to show that the number of iterations of the loop is finite.

$\displaystyle\Sigma\vdash{P}\ \mathbf{sat}\ {\langle
loopinv(\alpha)\cap\\{\mkern-4.5mu\mid{\alpha>0}\mid\mkern-4.5mu\\},R,G,\exists\beta<\alpha.\
loopinv(\beta)\rangle}$ $\displaystyle\wedge
loopinv(\alpha)\cap\\{\mkern-4.5mu\mid{\alpha>0}\mid\mkern-4.5mu\\}\subseteq\\{\mkern-4.5mu\mid{b}\mid\mkern-4.5mu\\}\wedge
loopinv(0)\subseteq\\{\mkern-4.5mu\mid{\neg b}\mid\mkern-4.5mu\\}$
$\displaystyle\wedge\forall s\in loopinv(\alpha).\ (s,t)\in
R\longrightarrow\exists\beta\leqslant\alpha.\ t\in loopinv(\beta)$

For instance, to prove termination of the loop statement in _free_block_ shown
in Fig. 9, we define the loop invariant with the logical variable $\alpha$ as
follows. Here,
${\emph{$\mathopen{\\{\mkern-4.5mu\mid}$}}{\emph{\'{\relax}}}inv{\emph{$\mathclose{\mid\mkern-4.5mu\\}}$}}$
defines a set of states, each of which satisfies the $inv$ predicate. It is
equivalent to $\\{s.\ inv\ s\\}$.

_mp -free-loopinv_ t b  _$\alpha$_  _$\equiv$_
_$\mathopen{\\{\mkern-4.5mu\mid}$_ … _$\wedge$__´_ inv _$\wedge$_ level b  _$
<$_ length  _$($__´_ lsizes t _$)$_

_$\wedge$_  _$($__$\forall\,$_ ii _$ <$_length  _$($__´_ lsizes t
_$)$__$\mathord{.}$_  _´_ lsizes t  _$!$_ ii  _$=$_  _$($_ max-sz  _$($__´_
mem-pool-info  _$($_ pool b _$)$__$)$__$)$_ div  _$($_ 4 ^ ii _$)$__$)$_

_$\wedge$_  _´_ bn t  _$ <$_ length  _$($_ bits  _$($_ levels  _$($__´_ mem-
pool-info  _$($_ pool b _$)$__$)$__$!$__$($__´_ lvl t _$)$__$)$__$)$_

_$\wedge$_  _´_ bn t  _$=$_  _$($_ block b _$)$_ div  _$($_ 4 ^  _$($_ level b
_$-$_  _´_ lvl t _$)$__$)$_ _$\wedge$_ _´_ lvl t  _$\leq$_ level b

_$\wedge$_  _$($__´_ free-block-r t  _$\longrightarrow$_ _$($__$\exists\,$_
blk _$\mathord{.}$_  _´_ freeing-node t  _$=$_ Some blk  _$\wedge$_ pool blk
_$=$_ pool b

_$\wedge$_ level blk  _$=$_  _´_ lvl t  _$\wedge$_ block blk  _$=$_  _´_ bn t
_$)$_

_$\wedge$_  _´_ alloc-memblk-data-valid  _$($_ pool b _$)$_  _$($_ the
_$($__´_ freeing-node t _$)$__$)$__$)$_

_$\wedge$_  _$($__$\neg$_  _´_ free-block-r t  _$\longrightarrow$_  _´_
freeing-node t  _$=$_ None _$)$_  _$\mathclose{\mid\mkern-4.5mu\\}}$_
_$\cap$_

_$\mathopen{\\{\mkern-4.5mu\mid}$_  _$\alpha$_  _$=$_  _$($_ if  _´_ freeing-
node t  _$\not=$_ None then  _´_ lvl t  _$+$_ 1 else 0 _$)$_
_$\mathclose{\mid\mkern-4.5mu\\}}$_

where $freeing\\_node$ and $lvt$ are local variables respectively storing the
node being free and the level that the node belongs to. In the body of the
loop, if $lvl\ t\ {\emph{$>$}}\ {0}$ and $partner\\_bit$ is _true_ , then
$lvl=lvl-1$ at the end of the body. Otherwise, $freeing\\_node\ t=None$. So at
the end of the loop body, $\alpha$ decreases or $\alpha=0$. If $\alpha=0$, we
have $freeing\\_node\ t=None$, and thus the negation of the loop condition
$\neg free\\_block\\_r\ t$, concluding termination of _free_block_.

Due to concurrency, it is necessary to consider fairness to prove termination
of the loop statement in _k_mempool_alloc_ from Line 34 to 47 in Fig. 3. On
one hand, when a thread requests a memory block in the _FOREVER_ mode, it is
possible that there will never be available blocks since other threads do not
release allocated blocks. On the other hand, even when other threads release
blocks, it is possible that the available blocks are always raced by threads.

###  6.4. Proof of Safety

We have proved the following theorem to show that, as a closed system, the
memory management of Zephyr is safe w.r.t invariant $inv$ executing from an
initial state $s_{0}$. According to Theorem 2.1, the memory management also
preserves the safety in any environment $R$, if $R$ is stable with the
invariant.

###### Theorem 6.4 (Safety of Memory Management).

The PiCore specification _Mem_Spec_ in Equation (1) satisfies the invariant
_inv_ w.r.t. the initial state $s_{0}$ in an empty environment $\\{\\}$.

###### Proof.

To prove the theorem, by Theorem 2.1 and Theorem 6.1, we only need to show
that $inv(s_{0})$, $stable(\\{s.\ inv(s)\\},\\{\\})$, and $stable(\\{s.\
inv(s)\\},Guar)$ where $Guar$ is defined in Theorem 6.1. The first two
predicates are obviously satisfied as we have shown before. The third
predicate is satisfied since $Mem\\_pool\\_guar\ t$ is stable with the
invariant and the guarantee conditions of $tick$ and $schedule$ do not change
the memory. ∎

###  6.5. Proof of Security

To apply the compositional reasoning approach to proof integrity of a parallel
event system, we instantiate the security configuration in Section 5.2 for the
specification of the memory management, i.e. $Mem\\_Spec$ in Equation (1).

The $\leadsto$ relation of domains is instantiated as the _interference_
function as follows. The first two rules mean that the Timer can only
interfere itself. The third rule means that a thread can interfere with itself
but not other threads. The _scheduler_ can interfere with all threads and the
_timer_. A special case in the memory management of Zephyr is that threads can
interfere with the _scheduler_ too, because the memory allocation service may
block the current thread and reschedule to other threads. It is very different
from the interference relation in separation kernels (e.g. (Murray et al.,
2013)) and ARINC 653 OSs (e.g. (Zhao et al., 2019b)), where the scheduler must
not be interfered by partitions or processes for the purpose of temporal
separation.

$\left\\{\begin{aligned} &\textbf{Timer}\leadsto c=(c=Timer)\\\
&c\leadsto\textbf{Timer}=(c=Timer)\\\ &(\textbf{\emph{$\mathcal{T}$}}\
t)\leadsto(\textbf{\emph{$\mathcal{T}$}}\ r)=(t=r)\\\
&otherwise...=True\end{aligned}\right.$

The state equivalence relation $s\stackrel{{\scriptstyle{d}}}{{\sim}}r$ is
instantiated as follows. It requires that two states are equivalent to a
thread _t_ iff the allocated memory blocks of _t_ in the two states are the
same.

$\left\\{\begin{aligned}
&s\stackrel{{\scriptstyle{\textbf{\emph{$\mathcal{S}$}}}}}{{\sim}}r=(cur\
s=cur\ r)\\\ &s\stackrel{{\scriptstyle{(\textbf{\emph{$\mathcal{T}$}}\
t)}}}{{\sim}}r=(mblocks\ s\ t=mblocks\ r\ t)\\\
&s\stackrel{{\scriptstyle{\textbf{Timer}}}}{{\sim}}r=(tick\ s=tick\
r)\end{aligned}\right.$

The domain function _dom_e_ is instantiated as follows, which is
straightforward.

$\left\\{\begin{aligned} &dom\\_e\ s\ (\textbf{\emph{$\mathcal{T}$}}\ t)\
(alloc(p,sz,to)@t)=\textbf{\emph{$\mathcal{T}$}}\ t\\\ &dom\\_e\ s\
(\textbf{\emph{$\mathcal{T}$}}\ t)\ (free(b)@t)=\textbf{\emph{$\mathcal{T}$}}\
t\\\ &dom\\_e\ s\ \textbf{\emph{$\mathcal{S}$}}\
(schedule(t))=\textbf{\emph{$\mathcal{S}$}}\\\ &dom\\_e\ s\ \textbf{Timer}\
tick=\textbf{Timer}\end{aligned}\right.$

By the compositional reasoning approach in Section 5.3, to prove the integrity
of the memory management of Zephyr, we first have to show the integrity of
memory services shown as the following lemma.

###### Lemma 6.5 (Integrity of Memory Services).

$\forall ev\ u\ s_{1}\ s_{2}\ k.\ ev\in evts(Mem\\_Spec)\wedge(s_{1},s_{2})\in
G_{\Gamma(ev)}\wedge(dom\\_e\ s_{1}\ k\
ev)\mathrel{\mathchoice{{\ooalign{$\displaystyle/$\cr\hfil$\displaystyle\leadsto$\hfil\cr}}}{{\ooalign{$\textstyle/$\cr\hfil$\textstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptstyle/$\cr\hfil$\scriptstyle\leadsto$\hfil\cr}}}{{\ooalign{$\scriptscriptstyle/$\cr\hfil$\scriptscriptstyle\leadsto$\hfil\cr}}}}u\longrightarrow
s_{1}\ \stackrel{{\scriptstyle{u}}}{{\sim}}\ s_{2}$

###### Proof.

By $mem\\_Spec$ in Equation 1, the proof of this lemma is discharged by cases
of $ev$ and then induction of the domain $u$.

  * •

if $ev$ is an event $Mem\\_pool\\_alloc$ or $Mem\\_pool\\_free$, then
$dom\\_e\ s_{1}\ k\ ev$ is a thread $t$.

    * –

if $u$ is the scheduler, then its proved since $t$ can interfere with the
scheduler.

    * –

if $u$ is the timer, then its proved since the execution of memory services
does not change the $tick$ variable.

    * –

if $u$ is a thread $r$, then we have $t\neq r$. It is proved by that the
memory separation property in the guarantee condition _Mem -pool-guar_ does
not change the allocated memory of other threads.

  * •

if $ev$ is the $schedule$ event, then $dom\\_e\ s_{1}\ k\ ev$ is the scheduler
_$\mathcal{S}$_.

    * –

if $u$ is the scheduler, then its proved since a domain can interfere with
itself.

    * –

if $u$ is the timer, then its proved since the $schedule$ event does not
change the $tick$ variable.

    * –

if $u$ is a thread $t$, then its proved since the $schedule$ event does not
change the memory.

  * •

if $ev$ is the $tick$ event, then its proved since the $tick$ event does not
change the current thread and the memory.

∎

Finally, we have the following theorem to show the integrity of the memory
management.

###### Theorem 6.6 (Integrity of Memory Management).

The PiCore specification _Mem_Spec_ in Equation (1) satisfies the integrity
property.

###### Proof.

The proof is straightforward by Theorem 5.7, Theorem 6.1 and Lemma 6.5. The
rest to prove is $\forall ev\in evts(Mem\\_Spec).\ is\\_basic(ev)$, which is
straightforward since the events are all basic events according to the
definition of $Mem\\_Spec$. ∎

##  7\. Result and Evaluation

###  7.1. Verification Effort

The verification conducted in this work is on Zephyr v1.8.0. The C code of the
buddy memory management is $\approx$ 400 lines, not counting blank lines and
comments. Table 1 shows the statistics for the effort and size of the proofs
in the Isabelle/HOL theorem prover. In total, the models and mechanized
verification consists of $\approx$ 34,000 lines of specification and proofs
(LOSP), and the total effort is $\approx$ 26 person-months (PM), where the
security proof in PiCore takes 4 PMs. The specification and proof of PiCore
are reusable for the verification of other systems. We develop $\approx$
18,200 LOSP for the concurrent memory management of Zephyr, 40 times more than
the lines of the C code due to the in-kernel concurrency, where invariant
proofs represent the largest part. This takes 14 PMs. Since the safety and
security properties are represented by the guarantee conditions of the memory
management services, the final theorems to show the safety and security are
relatively small, taking 400 LOSP.

Table 1. Specification and Proof Statistics PiCore Language | Memory Management
---|---
Item | LOSP | PM | Item | LOSP | PM
Language and Proof Rules | 700 | 8 | Specification | 400 | 14
Lemmas of Language/Semantics | 3,000 | Auxiliary Lemmas/Invariant | 1,700
Soundness | 7,100 | Rely-guarantee Proof of Allocation | 10,700
Invariant | 100 | Rely-guarantee Proof of Free | 5,000
Security | 4,800 | 4 | Proof of Safety and Security | 400
Total | 15,700 | 12 | Total | 18,200 | 14

###  7.2. Bugs Found in Zephyr

During the formal verification, we found 3 bugs in the C code of Zephyr. The
first two bugs are critical and have been repaired in the latest release of
Zephyr. To avoid the third one, callers to _k_mem_pool_alloc_ have to
constrain the argument _t_size size_.

(1) Incorrect block split: this bug is located in the loop in Line 20 of the
_k_mem_pool_alloc_ service, shown in Fig. 3. The _level_empty_ function checks
if a pool $p$ has blocks in the free list at level _alloc_l_. Concurrent
threads may release a memory block at that level, making the call to
_level_empty(p, alloc_l)_ to return _false_ and stopping the loop. In such
case, it allocates a memory block of a bigger capacity at a level $i$ but it
still sets the level number of the block as _alloc_l_ at Line 23. The service
allocates a larger block to the requesting thread causing an internal
fragmentation of $max\\_sz/4^{i}-max\\_sz/4^{alloc\\_l}$ bytes. When this
block is released, it will be inserted into the free list at level _alloc_l_ ,
but not at level $i$, causing an external fragmentation of
$max\\_sz/4^{i}-max\\_sz/4^{alloc\\_l}$. The bug is fixed by removing the
condition _level_empty(p, alloc_l)_ in our specification.

(2) Incorrect return from _k_mem_pool_alloc_ : this bug is found at Line 36 in
Fig. 3. When a suitable free block is allocated by another thread, the
_pool_alloc_ function returns _EAGAIN_ at Line 18 to ask the thread to retry
the allocation. When a thread invokes _k_mem_pool_alloc_ in _FOREVER_ mode and
this case happens, the service returns _EAGAIN_ immediately. However, a thread
invoking _k_mem_pool_alloc_ in _FOREVER_ mode should keep retrying when it
does not succeed. We repair the bug by removing the condition $ret==EAGAIN$ at
Line 36. As explained in the comments of the C Code, _EAGAIN_ should not be
returned to threads invoking the service. Moreover, the _return EAGAIN_ at
Line 48 is actually the case of time out. Thus, we introduce a new return code
_ETIMEOUT_ in our specification.

(3) Non-termination of _k_mem_pool_alloc_ : we have discussed that the loop
statement at Lines 34 - 47 in Fig. 3 does not terminate. However, it should
terminate in certain cases, which are actually violated in the C code. When a
thread requests a memory block in _FOREVER_ mode and the requested size is
larger than _max_sz_ , the maximum size of blocks, the loop at Lines 34 - 47
in Fig. 3 never finishes since _pool_alloc_ always returns _ENOMEM_. The
reason is that the “ _return ENOMEM_ ” at Line 15 does not distinguish two
cases, $alloc\\_l<0$ and $free\\_l<0$. In the first case, the requested size
is larger than _max_sz_ and the kernel service should return immediately. In
the second case, there are no free blocks larger than the requested size and
the service tries forever until some free block available. We repair the bug
by splitting the _if_ statement at Lines 13 - 16 into these two cases and
introducing a new return code _ESIZEERR_ in our specification. Then, we change
the condition at Line 36 to check that the returned value is _ESIZEERR_
instead of _ENOMEM_.

###  7.3. Further Related Work

Klein et al. (Klein et al., 2009) presented the first formal verification of
the functional correctness and security properties of a general-purpose OS
kernel in Isabelle/HOL took roughly 20 person years for 10,000 lines of C
code. To reduce the cost of formal verification, Yang and Hawblitzel (Yang and
Hawblitzel, 2011) demonstrated mechanical verification of Verve, an operating
system and run-time system to ensure both the safety and correctness using
Boogie and the Z3 SMT solver, which only 2-3 lines of proof annotation per
executable statement. Nelson et al. (Nelson et al., 2017) proposed an approach
to designing, implementing, and formally verifying the functional correctness
of Hyperkernel with a high degree of proof automation and low proof burden
with the Z3 SMT solver. However, all these works did not consider concurrent
OS kernels.

Examples of recent progress in formal verification of concurrent OS kernels
are CertiKOS with multicore support (Gu et al., 2016), a practical
verification framework for preemptive OS kernels to reason about interrupts
(Xu et al., 2016), and a compositional verification of interruptible OS
kernels with device drivers (Chen et al., 2016). The Verisoft team
(Leinenbach, Dirk and Santen, Thomas, 2009; Alkassar, Eyad and Hillebrand,
Mark A. and Paul, Wolfgang and Petrova, Elena, 2010) applied the VCC framework
to formally verify Hyper-V, which is a widely deployed multiprocessor
hypervisor by Microsoft consisting of 100 kLOC of concurrent C code and 5 kLOC
of assembly.

To ease the formal verification, a large portion of related work make
assumptions on the targeted OS kernel. The formal verification of seL4 (Klein
et al., 2009) changed the C code of L4 microkernel and thus disabled the in-
kernel concurrency. Nelson et al. made the Hyperkernel (Nelson et al., 2017)
interface finite, avoiding unbounded loops, recursion, or complex data
structures. As opposed to brand new research systems developed for
verifiability (e.g. CertiKOS (Gu et al., 2016)), this article presented the
first verification of a 3rd-party existing and realistic concurrent OS. Our
formal specification in PiCore completely corresponds to the execution
behavior with fine-grained concurrency of the Zephyr C code.

Formal verification of OS memory management has been studied in sequential and
concurrent OS kernels, such as CertiKOS (Vaynberg and Shao, 2012; Gu et al.,
2016), seL4 (Klein and Tuch, 2004; Klein et al., 2009), Verisoft (Alkassar et
al., 2008), and in the hypervisors from (Blanchard et al., 2015; Bolignano et
al., 2016), where only the works in (Gu et al., 2016; Blanchard et al., 2015)
considered concurrency. Comparing to buddy memory allocation, the data
structures and algorithms verified in (Gu et al., 2016) are relatively
simpler, without block split/coalescence and multiple levels of free lists and
bitmaps. The work in (Blanchard et al., 2015) only considered virtual mapping
but not allocation or deallocation of memory areas.

Algorithms and implementations of dynamic memory allocation have been formally
specified and verified in an extensive number of works (Yu et al., 2003; Fang
and Sighireanu, 2017a; Marti et al., 2006; Su et al., 2016; Fang and
Sighireanu, 2017b; Fang et al., 2018). However, the buddy memory allocation
was only studied in (Fang et al., 2018), which did not consider concrete data
structures (e.g. bitmaps) and concurrency. A memory model (Saraswat et al.,
2007) provides the necessary abstraction to separate the behaviour of a
program from the behaviour of the memory it reads and writes. There are many
formalizations of memory models in the literature, e.g., (Leroy and Blazy,
2008; Tews et al., 2009; Gallardo et al., 2009; Ševčík et al., 2013; Mansky et
al., 2015), where some of them only created an abstract specification of the
services for memory allocation and release (Gallardo et al., 2009; Ševčík et
al., 2013; Mansky et al., 2015). Our article presents the first formal
specification and mechanized proof for concurrent memory allocation of a
realistic operating system.

Integrity is a sort of information-flow security (IFS) which deals with the
problem of preventing improper release and modification of information in
complex systems. Language-based IFS (Sabelfeld and Myers, 2003) defines
security policies on programming languages and concerns the data
confidentiality among program variables. Compositional verification of
language-based IFS has been conducted in (Mantel et al., 2011; Murray et al.,
2016; Murray et al., 2018). Formal verification of IFS on OS kernels need to
considers the events (e.g. kernel services, interrupt handlers) rather than on
pure programs. Therefore, state-event IFS (Rushby, 1992; von Oheimb, 2004;
Murray et al., 2012) is usually applied to OS kernels (e.g. (Murray et al.,
2013; Dam et al., 2013; Costanzo et al., 2016; Zhao et al., 2019b)). However,
formal verification of state-event IFS for concurrent systems (e.g. OS
kernels) has not been addressed in literature. Our article presents the first
integrity verification of concurrent OS kernels.

###  7.4. Limitations and Discussion

The state of the art of formal verification of OS kernels focuses on the
implementation level (e.g. (Klein et al., 2009; Yang and Hawblitzel, 2011; Gu
et al., 2016; Nelson et al., 2017)). One limitation of this work is that
formal verification is enforced at the low-level design specification.

The first concern of this decision is that our work aims at the highest
evaluation assurance level (EAL 7) of Common Criteria (CC) (Criteria, 2017),
which was declared as the candidate standard for security certification by the
Zephyr project. With regard to the EAL 7, a main requirement of functional
specification addressed by formal methods is a complete formal and modular
design of Target of Evaluation (TOE) with security proofs, rather than
mandating the formal verification at source code level. In this article, we
develop a fine-grained low level formal specification of Zephyr. The
specification closely follows the Zephyr C code, and thus is able to do the
_code-to-spec_ review required by the EAL 7 evaluation, covering all the data
structures and imperative statements present in the implementation.

Second, formally verifying functional correctness, safety and security of
concurrent C programs, in particular the memory management of Zephyr, is not
well supported by the state of the art of C verifiers (e.g. VCC (Kroening and
Tautschnig, 2014) (Cohen et al., 2009), Frame-C (Kirchner et al., 2015),
CBMC). _Simpl_ (Schirmer, 2006) is a generic imperative language embedded into
Isabelle/HOL that was designed as an intermediate language for program
verification. In the seL4 project, the C code was translated into _Simpl_ and
then a state monad representation by the _CParser_ and _AutoCorres_ tools,
which do not support concurrent C programs. Though we have extended _Simpl_ to
_CSimpl_ by concurrent statements and a rely-guarantee proof system in (Sanán
et al., 2017), a new parser for _CSimpl_ is still under development.

Another limitation and thus a challenge for concurrent OS kernels is
scalability. Our work has been carried out in the Isabelle/HOL interactive
theorem prover, and thus is labor-intensive. We developed specification and
proof, 40 times more than the lines of the C code due to the in-kernel
concurrency, where the complicated invariant proofs represent the largest
part. It is certainly that Isabelle/HOL has high degree of proof automation by
integrating various SMT solvers and automatic provers. Proof automation for OS
kernels has been made significant progress in recent years, successful
examples of this direction are (Yang and Hawblitzel, 2011; Nelson et al.,
2017) closely reaching 100%. However, automatic verification of concurrent OS
kernels is still a challenging (Nelson et al., 2017). Moreover, higher degree
of automation implies simpler specification or properties of kernels. For
instance, to enable automated verification with SMT solvers, Nelson et al.
made the Hyperkernel interface finite, avoiding unbounded loops, recursion, or
complex data structures.

With regards to security, currently PiCore only supports integrity of
concurrent reactive systems. In order for PiCore to support confidentiality,
it is necessary some modification on its core, and more specifically in the
labels associated with actions. This change allows the security framework to
obtain the necessary information to properly generate the possible parallel
execution traces. Additionally, seeking compositional reasoning at both the
security (by applying the step consistency unwinding condition), and
concurrent (by applying rely-guarantee) levels, we are adding a simulation
framework for PiCore similar to CSim2 for CSimpl (Sanan et al., 2021). This
new framework will provide a new set of inference rules for the compositional
verification of confidentiality preservation of PiCore specifications.

Finally, for the purpose of EAL7 evaluation of the concurrent Zephyr RTOS,
modular compositionality of the specification and proof is a necessary
approach, such as the technique of certified abstract layers (Gu et al., 2015,
2018). Due to the concept of “event” in PiCore and their sequential
composition for event systems as well as their parallel composition for the
whole system, the formal specification of PiCore is compositional. Moreover,
the formal proof is compositional as well thanks to the compositional
reasoning approach in the PiCore proof system for functional correctness,
safety and security.

##  8\. Conclusion and Future Work

In this article, we have developed a formal specification at low-level design
of the concurrent buddy memory management of Zephyr RTOS. Using the rely-
guarantee technique in the PiCore framework, we have formally verified a set
of critical properties for OS kernels such as correctness, safety and
security. Finally, we identified some critical bugs in the C code of Zephyr.

Our work explores the challenges and cost of certifying concurrent OSs for the
highest-level assurance. The definition of properties and rely-guarantee
relations is complex and the verification task becomes expensive. We used
$\approx$ 40 times of LOS/LOP than the C code at low-level design. Next, we
are planning to verify other modules of Zephyr, which may be easier due to
simpler data structures and algorithms. We are also working on extending
PiCore to support verification of confidentiality on concurrent reactive
systems, which together with the already supported integrity, will allow to
verify non-interference of PiCore specifications. For the purpose of fully
formal verification of OSs at source code level, we will replace the
imperative language in PiCore by a more expressive one and add a verification
condition generator (VCG) to reduce the cost of the verification. To improve
modularity, we are also working on horizontal verification, in order to
compose the state of different modules of OS kernels whilst making few changes
to the functional specification and formal proof.

## References

  * (1)
  * Alkassar et al. (2008) Eyad Alkassar, Norbert Schirmer, and Artem Starostin. 2008\.  Formal Pervasive Verification of a Paging Mechanism. In _Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_. Springer Berlin Heidelberg, Berlin, Heidelberg, 109–123.
  * Alkassar, Eyad and Hillebrand, Mark A. and Paul, Wolfgang and Petrova, Elena (2010) Alkassar, Eyad and Hillebrand, Mark A. and Paul, Wolfgang and Petrova, Elena. 2010.  Automated Verification of a Small Hypervisor. In _Proceedings of International Conference on Verified Software: Theories, Tools, and Experiments_. Springer Berlin Heidelberg, Berlin, Heidelberg, 40–54.
  * Andronick et al. (2015) June Andronick, Corey Lewis, and Carroll Morgan. 2015\.  Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System. In _Proceedings Workshop on Models for Formal Analysis of Real Systems (MARS)_. 10–24.
  * Blanchard et al. (2015) Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, and Frédéeric Loulergue. 2015\.  A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. In _Proceedings of International Workshop on Formal Methods for Industrial Critical Systems_. Springer International Publishing, 15–30.
  * Bolignano et al. (2016) Pauline Bolignano, Thomas Jensen, and Vincent Siles. 2016\.  Modeling and Abstraction of Memory Management in a Hypervisor. In _Proceedings of International Conference on Fundamental Approaches to Software Engineering (FASE)_. Springer Berlin Heidelberg, 214–230.
  * Chen et al. (2016) Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. 2016.  Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. In _Proceedings of 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)_. ACM, 431–447.
  * Cohen et al. (2009) Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009.  VCC: A Practical System for Verifying Concurrent C. In _Theorem Proving in Higher Order Logics_ , Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 23–42.
  * Costanzo et al. (2016) David Costanzo, Zhong Shao, and Ronghui Gu. 2016.  End-to-end Verification of Information-flow Security for C and Assembly Programs. In _Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation_ _(PLDI ’16)_. ACM, New York, NY, USA, 648–664.
  * Criteria (2017) Common Criteria. 2017\.  Common Criteria for Information Technology Security Evaluation (v3.1, Release 5).  https://www.commoncriteriaportal.org/.
  * Dam et al. (2013) Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati, and Oliver Schwarz. 2013\.  Formal Verification of Information Flow Security for a Simple Arm-based Separation Kernel. In _Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security_ _(CCS ’13)_. ACM, New York, NY, USA, 223–234.