Unambiguous Encapsulation

A couple days ago, Dominic Spill and Michael Ossman presented an interesting talk at Shmoocon on using specially crafted error correcting codes to have unambiguous encapsulation, preventing attacks like “Packet in Packet.” This appears to be the culmination of some work that was first proposed to the LANGSEC mailing list back in March. The underlying problem that they are trying to address is that the physical layer is almost always error-prone: bits often get flipped. The data link layer addresses this by using error-correcting codes: methods of encoding the bits to be transmitted such that certain types of errors can be caught and corrected, at the expense of some additional bandwidth overhead.

Packet in Packet Attacks

If a sufficient number of bit-errors occur, however, error correcting codes can still fail to correct or even detect an error. Protocols usually address this by adding a checksum in the packet header/preamble. To illustrate this, let’s consider a made-up link layer protocol in which there is a header that starts with the magic number 0x1337 followed by a checksum and the message body. If a detectable but uncorrectable error occurs, then the packet can be dropped. If an undetected bit-error occurs in the body, then the checksum will fail and the packet will be dropped. If an undetected error occurs in the header, then either the magic will be broken and it will fail to be detected as a frame or the checksum will fail, in both cases causing the packet to be dropped. The one exception to this latter case is the basis for Packet in Packet attacks: If we were to start the message body with 0x1337 followed by a checksum and our desired body, then the link layer protocol will skip over the corrupted header and think that the actual frame starts at the beginning of our hand-crafted body! In effect, we have embedded a complete packet inside the body of another. It turns out that if we transmit this carefully crafted packet-in-a-packet a bunch of times, then eventually (in what turns out to be a reasonable amount of time) a bit-error will occur causing our payload to be interpreted as the real link layer frame. Attacks like this have been demonstrated on real data link layer protocols like IEEE 802.15.4.

Isolated Complementary Binary Linear Block Codes

Spill and Ossman propose using a special error correcting code that has a property they call “isolation:” the code can be split into multiple subcodes that have additional error-correcting properties between them. One of the subcodes could be used strictly for bits of the header/preamble, while another subcode could be used strictly for the body. This provides additional error correcting capability specifically for cases like that which the attack above exploits, without increasing the bandwidth overhead of the code. They call this family of codes “Isolated Complementary Binary Linear Block Codes” (ICBLBC).

As an example, consider the following eight code words:

00000	00011	00101	01001
01110	10110	11010	11100

Note that each code word differs from the others by at least two bits. This means that we can detect single-bit errors. For example, if 01110 is corrupted in the physical layer to 01010, then we can immediately know that an error occurred because that code does not exist in our set of eight. If two or more bit-errors occur, then an error may go undetected, which is the case that Packet in Packet attacks exploit. This is exactly like the types of error correcting codes used in most data link layer protocols. The difference, however, is that this particular set of eight code words has an additional property: it is an isolated complementary binary linear block code. Let’s call the first row of codes “Subcode 1” and the second row of codes “Subcode 2.” Now, note that every code in Subcode 1 differs from every other code in Subcode 2 by at least three bits. That means that we can not only detect but also correct single-bit errors between the two codes, giving the two subcodes properties of a Hamming Code. If we encode the header/preamble of the packet using one subcode and the body using the other, then we can circumvent Packet in Packet attacks with little to no extra bandwidth overhead!

Generating the Codes

Spill and Ossman have provided some code that can enumerate these codes. Currently, they have reported discovery of 6-bit ICBLBCs with up to twenty-two codes in subcode 1 and two codes in subcode 2, or up to ten codes in each if they are divided evenly. While their implementation does work, it is limited by the fact that it essentially performs a brute-force search to discover them, causing them to investigate a hardware-based approach using FPGAs.

Out of curiosity, I wondered if this problem could be solved more efficiently using constraint reasoning. Therefore, we implemented a generator that encodes the ICBLBC constraints as a Satisfiability Modulo Theories problem and used DOCO (Digital Operatives’ proprietary constraint optimizer) to enumerate all feasible solution codes. Sure enough, our solver was able to almost instantaneously reproduce Spill and Ossman’s results, as well as enumerate codes of larger bit length that would likely be intractable to discover using brute force search. For example, in less than a second it was able to discover this 7-bit ICBLBC consisting of fifty codes in subcode 1 and two codes in subcode 2:

Subcode 1	Subcode 2
37, 118, 44, 21, 35, 28, 107, 61, 41, 25, 94, 13, 56, 84, 124, 31, 110, 117, 50, 76, 62, 49, 47, 81, 7, 19, 109, 87, 103, 22, 93, 82, 70, 26, 127, 115, 55, 52, 59, 73, 11, 91, 88, 67, 69, 42, 121, 14, 38, 122	0, 96

as well as this one with nineteen codes in each subcode:

Subcode 1	Subcode 2
23, 89, 17, 27, 9, 65, 51, 5, 83, 85, 0, 18, 80, 54, 36, 33, 113, 3, 116	76, 122, 61, 127, 103, 14, 107, 104, 79, 56, 109, 98, 28, 70, 94, 47, 110, 74, 42

This 8-bit ICBLBC was discovered in a matter of seconds and consists of eighty codes in one subcode:

Subcode 1	Subcode 2
1, 4, 7, 8, 13, 16, 19, 25, 30, 32, 35, 37, 41, 42, 44, 47, 49, 54, 56, 59, 61, 69, 76, 81, 84, 87, 88, 97, 100, 104, 109, 110, 112, 121, 122, 124, 127, 128, 131, 133, 137, 142, 145, 146, 148, 152, 155, 161, 162, 164, 168, 171, 173, 176, 179, 181, 185, 190, 193, 196, 199, 200, 205, 208, 211, 217, 218, 220, 223, 224, 227, 229, 233, 234, 236, 239, 241, 246, 248, 253	66, 75

I have reimplemented this approach using Microsoft’s “free” (as in beer) Z3 constraint solver and pushed it to a fork of Spill and Ossman’s project, available here. As always, feedback on this new approach is greatly appreciated.