Functional correctness

About WP

WP plugin is responsible for validate that a specific, formally described, subprogram contract is strictly respected by the given sub-program. The subprogram contract defines the way a subprogram behave, in terms of border effects (meaning any impact on inputs, output and external elements), for all possible input values and context when being executed.

As a subprogram behavior depends on the way child subprogram themselves behave, demonstrate a full correctness with WP require to demonstrate from leaf calls (without any external subprogram dependencies) to root call, naming the entrypoint or the library interface for libraries.

A typical WP program contract would look like:

Basic program contract for a statically forged table getter
 1  /*@
 2      behavior invalidid:
 3          assumes id >= SHM_LIST_SIZE;
 4          assigns \nothing;
 5          ensures \result == NULL;
 6      behavior validid:
 7          assumes id < SHM_LIST_SIZE;
 8          assigns \nothing;
 9          ensures \valid_read(\result);
10
11      complete behaviors;
12      disjoint behaviors;
13  */
14  shm_meta_t const *memory_shm_get_meta(size_t id)
15  {
16      shm_meta_t const *meta = NULL;
17      if (unlikely(id >= SHM_LIST_SIZE)) {
18          goto end;
19      }
20      meta = &shms[id];
21      /*@ assert \valid_read(meta); */
22  end:
23      return meta;
24  }

This is a typical leaf program, that is manipulating a build-time generated const table. The program specification is using behaviors for simplicity, using separated explicit program behaviors depending on its single input. Behaviors are then proven to be 1. strictly separated, 2. complete (no potential input exists that do not match any of the defined behaviors).

WP and composition-based correctness

The kernel is voluntary composed of libraries, meaning that each part of the kernel, from arch part to BSP implementation upto syscalls are separated libraries that depend on each-others through unified, build-independent interfaces specification.

This allows, for example, to substitute a given BSP with another without impacting other libraries. Another positive point is the enabling of compositional correctness :

Given a Sentry sub-library (e.g. libbsp), it is possible to demonstrate correctness of a library that use it by considering its interface specification only. Given that the current libbsp implementation has been separately proven to respect its own interface specification, it is then possible to demonstrate the other library implementation, based on the libbsp interface correctness as hypothesis.

Such model is efficient as:

  • it is possible to demonstrate faster each library separately, allowing parallelism

  • it is possible to hold multiple libbsp implementations (for e.g. for multiple SoCs) that can be demonstrated separately

  • it allows incremental proofness, when adding new implementations of the same interface, without breaking other components proofness

Note

For easy plugable implementation over unified interface, the usage of C aliases is used, in order to link the corresponding implementation over the local API

Correctness of hardware manipulation

Hardware manipulations are very low level specific behavior that are difficult to be considered for pure software correctness analysis, as hardware behavior is not a part of software analysis.

Nonetheless, it is possible, when using sufficient fine-grain correctness analysis to inform Frama-C that a given memory area (typically a io-mapped device) do exist and is accessible.

In Sentry, hardware accesses (typically register accesses) is made using uniquely defined API, such as iowrite32(size_t addr, uint32_t val). Such an implementation, considering usage of Frama-C is written as:

Typical low-level accessor
 1/*@
 2  assigns *(uint32_t*)addr;
 3  */
 4__attribute__((always_inline))
 5static inline void iowrite32(size_t addr, uint32_t val)
 6{
 7#ifdef __FRAMAC__
 8    *(uint32_t*)addr = val;
 9#else
10    __iowrite32(addr, val);
11#endif

}

In that case, the __iowrite32 symbol is not considered by Frama-C as it includes some hardware specific ASM implementation such as memory barrier or memory order arch-specific opcodes, that have now meaning for Frama-C.

Although, Frama-C is still able to considered that the address is effectively written, and do generate a border effect in the addr memory cell. Moreover, any register is considered as a volatile memory cell, meaning that any consecutive access may lead to uncontrolled value read, which is an over-definition of a register.

In a statistical way, belong all potential retrieved values from a register, some leads to error management paths (invalid register’s value from the driver point of vue), others to correct paths. This is costly but ensure that all potential paths can be triggered, whatever the register fields are (write/clear, etc.).

From SVD to generated predicates

Only defining a device as a basic memory area is not precise enough, and in Sentry, some supplementary checks are automatically forged, using the SVD file describing the hardware.

In sentry, a lot of predicates are automatically forged using SVD specification. This is done when generating all device register structure, address and fields from the SVD file. This is done using the svd2json python package which allows the usage of jinja2 syntax to forge C files.

A typically autogenerated predicate for a lpuart driver looks like:

Auto-generated device-related predicate
 1/*@
 2  predicate lpuart_is_writable_register(ℤ r) = (
 3      r == 0x0 ||
 4      r == 0x0 ||
 5      r == 0x4 ||
 6      r == 0x8 ||
 7      r == 0xc ||
 8      r == 0x18 ||
 9      r == 0x1c ||
10      r == 0x1c ||
11      r == 0x20 ||
12      r == 0x24 ||
13      r == 0x28 ||
14      r == 0x2c ||
15      r == 0x30 ||
16      \false
17  );
18*/

For all devices, the following predicate are defined:

  • <devname>_is_writable_register: the target offset-based memory started from the device address is writeable

  • <devname>_is_readable_register: the target offset-based memory started from the device address is readable

  • <devname>_register_exists: the target offset-based memory started from the device address is a real register

Using this three typical predicates, it is possible to:

  • demonstrate accesses to read-only, write-only and read-write registers (SVD conformity)

  • demonstrate that no potential memory hole that exists in the device is accedded

It is then possible to write code such as:

Driver implementation with functional proofness
 1/*@
 2   // MYDEVICE_BASE_ADDR is forged using SVD
 3   requires mydevice_register_exists(offset);
 4   requires mydevice_is_writeable_register(offset);
 5   assigns *(uint32_t*)(MYDEVICE_BASE + offset);
 6   // [...]
 7 */
 8void mydevice_register_write(size_t offset, uint32_t value)
 9{
10    iowrite32(MYDEVICE_BASE + offset, value);
11}

Note

By now, registers accessor are not generated, although, this can be easily done as all required information for register’s accessor exists in the SVD file

Based on this leaf implementation of register accessor plus iowrite32, it is then possible to define clean behaviors for upper layer API of a given device driver such as mydriver_probe(), mydriver_xmit() and so on.

When defining a public contract for a given library interface though, some internal-specific elements (private context manipulation, etc.) may requires to define separated public and private contracts than need to be unified at proof time. This may, then, requires to define higher grain, publicly defined behaviors, while local, private specific behavior are kept hidden from external callers, as they have no meaning out of the local compilation unit. The usage of ghost functions and ghost variables are a useful helper for such cases, so that sequential behaviors (context setting, locks, etc.) can be demonstrated through ghost code. As ghost code is specific to Frama-C execution, they do not impact the target execution.

Correctness of security model

Some specific critical security behaviors are also demonstrated, such as, for example, the W^X:

MPU configuration correctness analysis
 1__STATIC_FORCEINLINE kstatus_t mpu_forge_resource(const struct mpu_region_desc *desc,
 2                                                 layout_resource_t *resource)
 3{
 4  //[...]
 5  /*@ assert desc->noexec == 0 ==> desc->access_perm != MPU_REGION_PERM_FULL; */
 6  /*@ assert desc->access_perm == MPU_REGION_PERM_FULL ==> desc->noexec == 1; */
 7  resource->RBAR = ARM_MPU_RBAR(desc->id, desc->addr);
 8  resource->RASR = ARM_MPU_RASR_EX(desc->noexec ? 1UL : 0UL,
 9                         desc->access_perm,
10                         desc->access_attrs,
11                         desc->mask,
12                         desc->size);
13  //[...]

When using EVA to cover overall kernel paths (entrypoint and handlers), such a dual implication assertion allows to demonstrate that in any call stack, this subprogram is never called with both write and execute flags set at the same time, demonstrating the W^X property for both user and kernel spaces whatever the execution context is.

Such a behavior check is to be added for all security properties that are implemented in Sentry kernel.