Preserving the programmers ‘Intent’ in Unsafe Rust

A few weeks ago, I happen to revisit a ‘Rust’ project of mine — a barebones embedded bootloader, hoping to re-use and extend it. I chose ‘rust-lang’ (over C) to write a security-focused ‘cortex-m’ bootloader, so that I could take advantage of rust’s memory-safety properties (other considerations such as size and performance being equal).

My requirements for the bootloader were as follows — boot the system, interface with a hardware root of trust, verify a signed boot-image using ECC and perform ‘downloaded software upgrades’ (or DSU).

At first glance, this seemed relatively straightforward, given that I already have a PoC but soon realized that there are many ways for things to go wrong here. As an example, take the following snippet of code, it’s a tiny part of my original PoC that controls execution-flow from the bootloader to the application-image when provided with the application’s start-address.

Basic boot-jump sequence for an ARM Cortex-M system.

At the time of testing, I didn’t pay much attention to it but this implementation CAN do things that I didn’t intend for it to do.

1. De-referencing 2 raw pointers i.e. stack_pointer and reset_vector could lead to undefined behavior (i.e. dereferencing can produce any value).
2. Transmutation of a 32 bit integer to an extern C fn() type is again undefined, if we pass-in an invalid value.
3. 2 register writes with obvious side-effects is undefined, if you pass-in an invalid, null or some other crazy value.
4. And a transmuted function call — jump_vector()that actually diverges (i.e. never returns) but doesn’t explicitly say so in its function signature.

Most of the above may seem like a consequence of using ‘Unsafe Rust’. That is partly true but for the most part, you cant avoid it as there is no way for code to safely mutate HW i.e. code cant tell if HW operations like reads/writes are actually safe.

Also something to note — in Rust, all undefined behavior is limited in scope and can be confined to ‘Unsafe Rust’ and that’s a good thing.

So, although the above snippet works in a set of test runs, I can’t actually claim or provide guarantees about the implementation as it relates to security. In other words, this little piece of code may or may not work for every single boot-invocation.

*There goes my original (assumed simple) goal of extending the bootloader.

So, how do we ensure that we don’t end-up with undefined behavior at runtime. ARM Cortex-M has a flat memory (i.e. no virtual addressing) model and you have to explicitly state your program’s memory layout via a memory.x file. We could leverage our knowledge of an ARM Cortex-M system’s memory layout to define a specification and have our implementation adhere to it.

For instance, we could add a couple of defensive checks such as assert statements after each of the 2 derefs, to check for bounds but a better solution (in my opinion) is to have your types to do the `checking`.

• For the stack pointer — we could construct a type named ‘RefinedUsize’ using rust’s const_generics feature and apply the bounds check at runtime. In a way, this is an example of refinement types (i.e. types with predicates).

This could’ve been even better if we had a way of accessing linker-script values in our rust code which means we can avoid using concrete bounds or values. As of this writing, I’m unaware of the option to do so.

Also, in this specific case, we’re assuming RAM size of 256KB (zero-sized .data, .bss sections + no heap) and we’re using flip-link to avoid stack overruns.

• For the reset vector — RefinedUsize can refine a u32 down to a single valued u32.
• Constraining possible inputs of an integer type to a single non-nullable value and transmuting it is safe i.e. reset_vector is a u32 that can only have one possible value. Rust’s intrinsic function — transmute() can now convert a non-nullable, well sized and correctly aligned u32 to a function pointer.
• Add data and instruction synchronization barriers before the 2 volatile (register) writes to ensure that there are no pending memory accesses or instructions that can potentially interfere with our register writes.

Note — this still doesn’t mean your volatile write is guaranteed to succeed. But now, we can say its not undefined behavior if it does not succeed.

• Finally change jump_vector() and boot_from() ‘s type signatures to reflect divergence, which means it must never return (but can panic due to some HW register write error) and if it does return, then we know something went wrong. (i.e. undefined behavior)

Refactored impl using Rust’s const_generics feature to make our types more precise.

Now, this implementation is much better than the original PoC or at least it gives me a higher degree of confidence that my code will stick to my specification (provided in the form of type refinements).

We still cant make the claim that this type-enriched implementation is a guarantee (or an actual mathematical proof) for the absence of undefined behavior in the above snippet of code. For that kind of assurance, we need to be aiming for complete functional correctness, which can only be achieved through ‘Formal Methods’.

Formal Methods is a gargantuan field . Its actually a bit crazy, so here’s the pictorial summary from a programmer’s viewpoint.

A 20k foot view of the world of formal methods, from a programmers point of view.

In short, formal methods allow you to specify properties and verify conformance to it by either:

• enriching types — For example, refine/constrain the type of arguments passed to a function and have an automated theorem prover solve all constraints — much like what we’ve done above except the difference is that an automated theorem prover generates proofs that will hold under all possible conditions (i.e. pre, post conditions and all invariants).
• Or by writing a separate proof (formal term is lemma) for your function using something like a proof assistant tool, where you state properties and build a proof for it.

An example of such a property is —

(append (append xs ys) zs == append xs (append ys zs))

where append is a function that appends 2 lists and xs, yz, sz are lists of any type. This property must always hold true for all lists (for eternity :)). The proof for this property is pretty simple but with proof assistants, you can leverage more exotic types like dependent types, higher order logics, inductive proofs etc. to solve much trickier properties.

Wishlist and Conclusions:

• I think extending Rust’s type-system natively by making it easier to refine primitive types (i.e. int, char, bool) with a much nicer looking syntax — like x: int { x > 0 } ,rather than having a developer/library do the work, would be a logical next step post stabilization of const_generics.

What would be even more awesome is if rust-analyzer could show refinements in VSCode.

• A static verifier for Rust with support for pre + post conditions, invariants and variants that works with both safe and unsafe rust would truly be a godsend. In fact, Rust may already be on its way towards this goal; we have a couple of folks working on bringing automated reasoning capabilities to Rust. Here’s 2 of them.

Crux-mir: we can perform property-based testing, where we exhaustively test all possible inputs for a given function using symbolic simulation.

Haybale: this is similar in terms of the underlying tech but it uses symbolic execution to help you reason about Rust code.

• I plan to explore both, maybe in another post. Strictly speaking, these 2 don’t exactly fall into realm of formal verification . We can think of them as a form of testing on steroids. They can be used to exhaustively explore a program’s state-space i.e. you can test your code exhaustively for bugs. However, “testing can only find bugs, not prove their absence” , which is where formal verification comes-in; it provides actual proofs.

To conclude, this entire exercise has been quite rewarding in terms of the learning, I picked up a few lessons and techniques to help me ‘reason about code’ at a deeper level and answer questions about how to preserve my (i.e. programmers) ‘intent’ such that it is not cannibalized by a varied number of implementation-level details. For example, its always good to start with the most basic questions —

How safe/secure is my code really?

What claims can I make or should I make?

What guarantees can I provide?

This will allow you to clearly state simple properties about your code which can be proved with relative ease (with an automated prover) and then by the power of composition you can chain all of these properties (and proofs) giving you the ability to make an irrefutable (i.e. mathematically provable) claim.

Maybe, I can show a more concrete example in my next post, where I rewrite an AES crypto impl to match one implemented in Cryptol - a domain-specific language for specifying and verifying cryptographic algorithms.