Back
Featured image of post Type-Driven Development

Type-Driven Development

I wrote an IMAP parsing and serialization library and want to make it correct and misuse resistant by leveraging Rust's type system.

Hello, World!

I was recently reminded about Cunningham’s Law

“The best way to get the right answer on the internet is not to ask a question; it’s to post the wrong answer.”

– Ward Cunningham

… and it made me think.

During my Ph.D. I used Obsidian, an app to write and cross-reference Markdown documents, to sort my thoughts. However, I didn’t share most of it and never discussed it with a broader audience.

So I figured… why don’t I have a blog?

After wrestling with Zola for some hours and comically failing to configure a theme, I installed Hugo. No worries, Zola. I’ll try a second time in the future! Anyway… this is my blog now. Hosted under a HSTS preloaded .dev domain. Served by Caddy. Structured and styled by the pretty Stack theme.

In my first post, I will think aloud about some design decisions I made during the development of the imap-codec library.

Introduction

Motivation

imap-codec was born out of frustration. During a research project, I analyzed IMAP clients for certain behavior and had difficulties constructing syntactically valid IMAP messages. IMAP is… “branched.” Some syntax elements are required in one place and prohibited in another one. I often stared at hard-to-understand IMAP sessions. Sessions, where I was 100% sure that a response was correct and learned that it wasn’t.

I started imap-codec to gradually improve our tooling and to not make the same errors twice. And, somehow, I remained interested in it. But let me first introduce the domain we are working in.

Parsing and serialization

imap-codec is an IMAP parser and serializer. The task of a parser is to turn a sequence of bytes, an input, into a more useful data structure, an object. The parsed object provides easy access to the encoded information. The task of a serializer is to “flatten” a parsed object into a sequence of bytes again.

More concretely, imap-codec provides two parsers1, command and response, which turn a sequence of bytes (&[u8]), to either a Command or a Response object. For the serialization part, Command and Response provide an encode method (via the Encode trait), which turns the parsed objects into bytes.

We will focus on the command part only because it makes the post easier to understand (and write.) But all thoughts apply to other parsers and types as well.

Bytes to command and vice versa (example)

When a user inputs the byte sequence …

A123 select "InBoX"\r\n

… to the command parser …

let (cmd, _) = command(b"A123 select \"InBoX\"\r\n")
                 .unwrap();

… it returns a …

Command {
  tag: Tag("A123"),
  body: CommandBody::Select {
    mailbox: Mailbox::Inbox,
  }
}

… object.

When cmd.encode(...) is called, it generates the byte sequence …

A123 SELECT INBOX\r\n

To eliminate a source of confusion: IMAP commands are prefixed by a tag. We used A123 but could have also used FooBar1337. Even… <script>alert`XSS`</script>. (Yes, you can call a JavaScript function with a mere template literal. No, I don’t know why. Yes, this can be useful in attacks, e.g., in the ALPACA Attack.)

There isn’t really that much to tell about the usage of imap-codec as a parser. You feed it some bytes and get a fully-parsed and verified-to-be-sane object (and a remainder.) No callbacks. No shotgun parsing. But there is more happening that is not obvious at first glance.

Misuse resistance, correctness, tightness, …

The term “misuse resistance” is better-known in cryptography but can be used more broadly. Basically, it means that a developer can’t use your library in the “wrong way.” Using a cryptographic library in “the wrong way” can lead to severe security issues. But many things can be misused with varying consequences. For example, a library (or application) can become perplexing when it is easy to misuse. It’s not just about security.

Currently, I describe imap-codec as misuse resistant, and mean that you can’t produce a syntactically invalid or inconsistent IMAP message – even when you try really hard. But there’s more to it. The API encodes domain knowledge about IMAP. In a role of an email client/server developer who is not necessarily an IMAP expert, you will (hopefully) have a hard time screwing up.

But wait. You’re not the one who has commit rights for imap-codec, are you? You’re not supposed to just change the internals of imap-codec. There are people for that! If someone screws up with imap-codec, it is more likely to be me. So… where is my safety net?

Where is my safety net?

Misuse resistance can happen “on different levels.” You can make your API misuse resistant to your consumers but hard to maintain internally. Sure, you can be careful, but I’m not. I don’t want to be! With that attitude… I better have a good strategy to not make stupid mistakes. Thus, I use Rust’s type system as much as possible and cross my fingers that a good public-facing API evolves from that. Concretely, all types in imap-codec, i.e., all structs and enums, should be designed, so that inconsistent state is not representable.

I know I might bend the term “misuse resistance” here. I could use “correct”, or “tight”, instead. But who said that instantiation of types cannot be resistant to misuse?

Leveraging Rust’s type system

The above example …

Command {
  tag: Tag("A123"),
  body: CommandBody::Select {
    mailbox: Mailbox::Inbox,
  }
}

… shows two instances where imap-codec uses Rust’s type system to enforce invariants on the type level.

First, note how the tag is wrapped in a Tag struct and consider what would happen if a Command could be constructed like this:

let cmd = Command {
  // `&str` instead of `Tag`
  tag: "A123 X", 
  body: CommandBody::Select {
    // `&str` instead of `Mailbox`
    mailbox: "InBoX",
  }
};

Serialization of cmd would likely produce:

A123 X SELECT "InBoX"\r\n
     ^
     |
     error: no such command "X"

Obviously, the tag must not contain any whitespace. But &str is not made to enforce that. Thus, imap-codec has a Tag, a newtype wrapper of &str enforcing additional rules. Especially (but not exclusively) that no whitespace is allowed.

Second, note that the string "InBoX" is not contained in the parsed Command. Instead, the mailbox became Mailbox::Inbox which is serialized as INBOX (without the quotes.)

Unlike other folder names, the Inbox in IMAP is not case-sensitive. If the selected mailbox were saved as a string, a programmer would need to remember to check all cases of “inbox”. The infamous …

if "inbox" == mailbox.to_lowercase() {
  // ...
}

The Mailbox struct unifies all Inboxes to Mailbox::Inbox. Concretely, it is defined as …

enum Mailbox {
  Inbox,
  Other(MailboxOther),
}

… and there is no way in imap-codec to create a Mailbox::Other(...) that semantically denotes the Inbox.

C’mon, how bad can it be?

How bad was the recent Firefox outage? I don’t know. But mishandling case sensitivity is a real source of bugs. But, more importantly, as domain specialists, we encode our domain knowledge into the type.

imap-codec uses a lot of these constructs. Atom, Tag, Text, … Even NonEmptyVec<T> and NonZeroU32!

IMAP section specifiers (example)

The IMAP RFC defines a “section specifier” syntax to fetch only specific parts of an email. Here are some examples from the IMAP RFC:

HEADER        // Fetch header
TEXT          // Fetch text
1             // Fetch part 1
1.HEADER      // Fetch header of part 1
1.TEXT        // ...
...
5.3.4.HEADER  // ...
...

How should we design a type, say, Section, for that?

Our first attempt …

struct Section {
  path: Vec<u32>,
  kind: Option<Kind>,
}

enum Kind {
  Header,
  Text,
}

… should work. All examples can be constructed, e.g., …

// HEADER
Section {
  path: vec![],
  kind: Some(Kind::Header),
}

// ...                                               

// 1
Section {
  path: vec![1],
  kind: None,
}                

// ...                                               

// 5.3.4.HEADER
Section {
  path: vec![5, 3, 4],
  Some(Kind::Header),
}  

// ...

However, there is a problem. There exists an invalid combination of path and kind:

Section {
  path: vec![],
  kind: None
}

When this is encoded, it will likely result in an empty byte sequence. However, this violates the IMAP specification for a section specifier. Now, we can be careful to not let this happen. But we can do better by redesigning the Section type to ensure that this assignment is not representable in the Section type.

We can merge …

struct Section {
  path: Vec<u32>,
  kind: Option<Kind>,
}

… and …

enum Kind {
  Header,
  Text,
}

… to a single …

enum Section {
  Part {
    path: NonEmptyVec<u32>
  }
  Header {
    path: Vec<u32>
  }
  Text {
    path: Vec<u32>
  }
}

Now, our Section is either 1) a Part, in which case the path can not be empty, or 2) a Header or Text, in which case the path can be empty.

Later, we also learn from the IMAP RFC that the numeric path must not contain zeros! Let’s fix that, too. Our final Section type then becomes …

enum Section {
  Part {
    path: NonEmptyVec<NonZeroU32>
  }
  Header {
    path: Vec<NonZeroU32>
  }
  Text {
    path: Vec<NonZeroU32>
  }
}

Ideally, all struct’s and enums in imap-codec should provide this certain type of quality that any arbitrary assignment of fields should make sense. I saw this property called tightness by Pablo Mansanet. A decent term, if you ask me. Quinn Wilton described it as Programming with Types. And there is also the term “Type-Driven Development” used (or even introduced?) by the creator of Idris, Edwin Brady. There is even a book titled “Learn Type-Driven Development” by Yawar Amin and Kamon Ayeva. To be honest… I didn’t know about Type-Driven Development before. I thought this is just how you are supposed to write Rust!

Tight types can easily be generated

A nice benefit of tight types is that you can simply [derive(Arbitrary)]. This allows to easily generate crazy – but valid – messages. This is useful for testing: You can encode(...) arbitrarily generated objects into bytes to test the serialization logic. Afterward, you can parse the serialized bytes to test the parsing logic. And you can compare results to test for correctness. Have a look at this beautiful IMAP command and how imap-codec is fuzzed!

Conclusion

Thinking about every type might seem like overkill at first. But it is really not too much work and seems to pay off. And more importantly, I am (somewhat) confident that imap-codec is not affected by injection attacks, which may lead to adventurous security issues. (More on that in some later blog post.)

Rust’s type system, especially algebraic data types, is useful for enforcing invariants on the type level. A good library design can use the type system to encode domain knowledge – think about how Inbox is case-insensitive. While mistakes can still happen in the “design phase” – e.g., a software developer misunderstood something and enforced the wrong thing – later modifications to the library are less likely to violate invariants. This programming strategy helped me work on imap-codec, and I hope that new contributors will also benefit from this safety net.

Also, I feel that if you are willing to spend time on a standard, better encode all you learn into the types you use. You will inevitably forget most details, and it is only a question of time that you break something because of that.

While the direction for imap-codec is (somewhat) clear to me, there is still work to do. Currently, imap-codec exposes (too?) many details. I have some thoughts on why this can either be negative or positive for this kind of library. But I haven’t gotten enough feedback and didn’t have the time to think it through.

Appendix

Parser correctness and malleability

You may have noted that imap-codec did not “recreate” what it parsed – A123 select "InBoX" vs. A123 SELECT INBOX. But, ideally, we want that …

$$ \texttt{parse}(\texttt{serialize}(\texttt{object})) = \texttt{object} $$

… and …

$$ \texttt{serialize}(\texttt{parse}(\texttt{input})) = \texttt{input} $$

… for any object and any input. (Excluding the error case.)

Or, in other words, we want parsing and serialization to be inverse to each other. In this case, we call a parser/serializer combination correct.

Let’s think for a moment about what this means in practice. First, we see that it is pretty easy to write a correct parser. Lo and behold …

struct Object(&[u8]);

fn parse(input: &[u8]) -> Object {
  Object(input)
}

fn serialize(object: Object) -> &[u8] {
  object.0
}

… voila!

This parser/serializer combination is correct. But it is not useful. We just wrapped the input in an Object newtype to obtain another domain to map our input to. This shows that the definition of Object – or generally the domain we map our input to – is key to usability and correctness.

imap-codec is not correct

imap-codec’s parsers are not injective because they can map different bytes, input1 and input2, to the same object. This means that the parse function is not a bijection, which means that it cannot have an inverse, which means it can not be correct.

We could archive correctness by preserving all information from the input – even the semantically irrelevant information such as the casing of the “select” command. This is maybe required in “format-preserving” parsing but less useful in protocols.

IMAP is malleable, and there is not much we can do about it

Arguing with my security hat on, a data format (or protocol syntax specification) should be non-malleable. Non-malleability means that each message has a unique representation. If this is not the case, you must preserve irrelevant information to archive correctness. Thus, correctness is probably not what you should want from a protocol that is malleable.

Why do you care?

Because fuzzing! It’s cooler when you have correctness!

I wanted to use fuzz-testing in imap-codec to …

let object = lib_fuzzer_magic();
assert_eq!(parse(encode(object)), object);

and

let input = lib_fuzzer_magic();
assert_eq!(encode(parse(input)), input);

… but I needed to cheat!

Instead of checking that imap-codec can recreates what it has parsed – which it can’t because of malleability – I parse the serialized bytes again and compare the parsed objects …

let input  = lib_fuzzer_magic();   

let object = parse(input);
let output = serialize(object);
let cheat  = parse(output);

// Does not work ...
// assert_eq!(input, output);

// Cheating ...
assert_eq!(object, cheat);

Despite uncovering a few bugs, I am not quite sure what I test here exactly … For example, this test would not catch if I would screw up and always return the same (wrong) object in the parse function.


  1. A different parser is required in certain message flows. But command and response are the main entry points. ↩︎

Built with Hugo
Theme Stack designed by Jimmy