Menu
Where examples listed in a previous post become analyzable
A previous blog post showed a number of difficulties that can arise when analyzing low-level C code, specifically the kind of C code that accesses the representation of addresses. It also claimed that, in a serendipitous fashion, a unified solution had been developed within TrustInSoft Analyzer for this panel of difficulties.
TrustInSoft Analyzer provides analysis results that hold true “for all possible memory layouts”, and one part of how it achieves this is by using a symbolic representation for addresses. For instance, in the snippet program below, the value of p is computed as {{ &x }}
This is the simplest way of keeping precise track of the fact that it is the variable x that is modified on the fourth line and that the function f returns 2 on the fifth line.
This symbolic representation also accounts for offsets, so that if the address of a struct member or array element is taken the analyzer will remember where the memory access occurs. TrustInSoft Analyzer represents offsets in bytes so that, if each of char*-arithmetic, int*-arithmetic and uintptr_t-arithmetic is used in different branches of a program, and these branches subsequently converge, all the offsets will be expressed in the same unit and it makes sense to compute the union of their values:
int t[20];
char *choose_offset(unsigned choice) {
switch (choice) {
case 2: return t + 2;
case 3: return (char*)t + 12;
case 4: return (int*)((uintptr_t)t + 16);
}
return 0;
}
… If the analyzer has inferred that the argument choice can be 2 or 3 or 4, it will compute the value returned in the first branch as {{ &t + {8} }}, indicating an offset of 8 bytes. Similarly, the values returned in the second and third branches are computed respectively as {{ &t + {12} }} and {{ &t + {16} }}, so that the set of values that can be returned by the function is correctly computed as {{ &t + {8, 12, 16} }}, meaning an offset of 8, 12 or 16 bytes from the beginning of the array t in memory.
However, this choice of a very specialized symbolic representation does not allow the analyzer to keep track of computations involving base addresses beyond offset computations. As an example, in the computation below, all versions of TrustInSoft Analyzer lose track of how the integer value of &t was used in computing the value of the variable r:
uintptr_t r = 2 * (uintptr_t) &t;
Attempting to construct a symbolic formula in which “&t” appears as a formal variable for the value of r would be a dangerous slippery slope. For programs that compute a checksum over a buffer of data containing pointers (another common occurrence of code accessing the representation of pointers that I did not mention in the first post), it would not end well.
Earlier versions of TrustInSoft Analyzer would only tell you that the value of r is an arbitrary integer because it depends on the memory layout, and specifically that this integer depends on where the compiler and linker placed the variable t in memory. Even while rejecting the idea of representing 2 * &t as a symbolic expression with a formal variable representing the address of t, it was still possible to greatly improve the handling of programs that compute this sort of thing. The remainder of this blog post shows how we decided to do it.
The most recent versions of TrustInSoft Analyzer use the alignment constraint and the size of the type of a variable to infer the set of integer values the address of the variable can have. In the case of the above variable t, of type int[20], on a usual ILP32 target, the size is 80 and the alignment constraint is 4. TrustInSoft Analyzer computes the set of possible integer values for &t as [4 .. 4294967212],0%4. The lower bound is 4 because &t must compare unequal to NULL, which means that t cannot be placed at address 0. The upper bound is 4294967212 (that is, 2**32 – 84) because the offset t+20 is valid to compute (a so-called “one past the end” pointer) and must compare greater than t.
This allows the analyzer to produce more precise results when (uintptr_t)&t is used in a computation where the result does not fit the “base_address + offset” format. For r = 2 * (uintptr_t) &t;, the analyzer infers that while the exact value of r depends on the location of t in memory, it is guaranteed to be a multiple of 8 between 0 and 0xfffffff8.
It is also possible to annotate the program with some information about where the array t is intended to be placed in memory. This information would typically mirror the information provided in a linker script, and in fact the best way to use this feature would be by automatic translation from the linker script optionally used to constrain the memory layout at link-time.
The previous example becomes:
/* The array t is at an address that is a multiple of 4
between 4 and 1000: */
int t[20] __attribute__((tis_address("[4..1000],0%4")));
uintptr_t r = 2 * (uintptr_t) &t; And now the value of r is computed as a set which, certainly, continues to depend on where t is placed in memory and is labeled as such, but which now is guaranteed to be a multiple of 8 between 8 and 2000.
Note that this new feature alone allows handling in a precise fashion the constructs in the code that attempt to detect whether some function or data is in a certain range of addresses. Patterns extracted from various codebases we have been looking at recently were shown in the previous post:
if ((uintptr_t) p >= (uintptr_t) FLASH_START) &&
(uintptr_t) p < (uintptr_t) FLASH_END)) The memory blocks that p may point to when the above lines are executed simply need to be annotated with a tis_address attribute that indicates that the block is certainly, or certainly not, in the flash memory range, for the analyzer to be able to infer that the condition is certainly true or certainly false, and to follow only the relevant execution path in the code.
Similarly, thanks to the set of values automatically inferred from the type’s alignment, some alignment checks that are written following the pattern below will now automatically be inferred to succeed:
assert ((uintptr_t) p % 8 == 0); More importantly, the checks that won’t be automatically inferred to succeed may indicate a bug, where the required alignment is not guaranteed for the type of the pointed address.
As for the memcpy example that I alluded to in the previous blog post, I can clarify the kind of code pattern I meant by extracting code from musl-libc’s implementation, which contains exactly the kind of optimization I was referring to:
void *memcpy(void *restrict dest, const void *restrict src, size_t n)
{
unsigned char *d = dest;
const unsigned char *s = src;
...
typedef uint32_t __attribute__((__may_alias__)) u32;
uint32_t w, x;
for (; (uintptr_t)s % 4 && n; n--) *d++ = *s++;
if ((uintptr_t)d % 4 == 0) {
...
}
if (n >= 32) switch ((uintptr_t)d % 4) {
case 1:
...
break;
case 2:
...
break;
case 3:
...
break;
}
...
The first loop copies the first few characters from source to destination until the source pointer is aligned (this is the (uintptr_t)s % 4 part of the condition, which could have been written “(uintptr_t)s % 4 != 0 && n != 0” for clarity). After this loop, if the destination pointer is also aligned (the “(uintptr_t)d % 4 == 0” test), copying the remainder of the buffer word by word is simple. Otherwise, the source and destination pointers are never aligned at the same time. What the remaining code does, for each of the values 1, 2, 3 that “(uintptr_t)d % 4” can have, is a different loop that repeatedly builds the word to write to destination as the last bits of the previous source word and the first bits of the current source word.
It is possible to test what this implementation does when applied to aligned 30-byte source and destination buffers with the declarations below:
// Case 0-0
char my_src[30] __attribute__((tis_address("[4..0xfffffd0],0%4")));
char my_dst[30] __attribute__((tis_address("[4..0xfffffd0],0%4"))); Provided with this alignment information, TrustInSoft Analyzer automatically infers the values of (uintptr_t)s % 4 and (uintptr_t)d % 4 when s and d are offsets inside my_src and my_dst respectively at various stages of the interpretation of the function memcpy.
Testing this particular alignment case can be done with ASan, in which it is relatively easy to make allocate aligned buffers that are guarded by red zones on each side. However, to the best of my knowledge, it would be either very advanced usage or impossible to test the 15 other behaviors of this memcpy implementation with any available tool. In recent TrustInSoft Analyzer versions, it is as simple as repeating the analysis with the following declarations:
// Case 0-1
char my_src[30] __attribute__((tis_address("[4..0xfffffd0],0%4")));
char my_dst[30] __attribute__((tis_address("[5..0xfffffd1],1%4")));
...
// Case 1-0
char my_src[30] __attribute__((tis_address("[5..0xfffffd1],1%4")));
char my_dst[30] __attribute__((tis_address("[4..0xfffffd0],0%4")));
// Case 1-1
char my_src[30] __attribute__((tis_address("[5..0xfffffd1],1%4")));
char my_dst[30] __attribute__((tis_address("[5..0xfffffd1],1%4")));
...
// Case 3-2
char my_src[30] __attribute__((tis_address("[3..0xfffffcf],3%4")));
char my_dst[30] __attribute__((tis_address("[2..0xfffffce],2%4")));
// Case 3-3
char my_src[30] __attribute__((tis_address("[3..0xfffffcf],3%4")));
char my_dst[30] __attribute__((tis_address("[3..0xfffffcf],3%4"))); The insight here, for handling code that uses the low bits of known-aligned pointers as bonus storage, is that this information that the base b is aligned can be used to compute repr = (uintptr_t) &b | 1 as {{ &b + {1} }}. Later during execution, having managed to produce this precise form for the value of repr similarly allows repr & 1 to be evaluated as 1, and repr & ~ (uintptr_t)1 to be evaluated as {{ &b }}.
Understanding this pattern in particular allows TrustInSoft Analyzer, with the information that the addresses used for nodes are all of the form [4..0xfffffff0],0%4, to analyse precisely the code of a BDD implementation, and to both follow what the implementation is doing with the low bits of pointers, and also guarantee that the BDD implementation behaves deterministically, and in particular, independently of the memory layout, within the aforesaid constraint.
Another pattern is, with a 64-bit memory space, understanding that (uint32_t) &x can be represented as {{ &x }} if the possible representations for the address &x are all below 2**32 (this is an actual need that emerged during the analysis of bootloader code for a modern smartphone). The code is intended for the AArch64 ISA with 64-bit pointers, but some of the addresses that are manipulated by the code are within the first 4 GiB of memory and are stored as 32-bit values.
In the introduction of this two-part article, I referred to the numerous occasions, in past years, where we would have needed an analyzer that understood low-level uses of pointer representations, and we had worked around the problem instead of defining and implementing the unifying solution we finally came up with. Even this long wait did not prepare me for how immediately and broadly useful the new system would turn out to be once available. We immediately began alpha-testing it in analyses we conduct ourselves. In addition, while some TrustInSoft Analyzer users may read about it for the first time in this post, others just happened to ask about analyzing C code containing some of the constructs that can now be handled more precisely just as the tis_address feature had made its way into the latest released version, and these users had the privilege of trying it out (do not be jealous, this meant stumbling upon the last remaining limitations and ergonomic failures). It was a major overhaul, but thanks to all this testing, we are now making the final fixes and tweaks.
One reason for the immediate usefulness of the new capabilities may be circumstantial, with kernels and secure bootloaders, written in C and relying heavily on such low-level constructs, being in 2022 obvious targets for formal verification of the absence of the worst kinds of security vulnerabilities. Another reason may be, if I am allowed to be a bit optimistic, that the analysis of high-level C programs is already working well enough, with identified methodologies to alleviate the difficulties for the fundamentally difficult targets, that new TrustInSoft Analyzer users in the process of identifying the codebases to which it can be beneficial would naturally zoom through the high-level modules and arrive to the low-level ones, for which they had to ask if anything was possible.
Huisong Li, Anne Pacalet, Raphaël Rieu-Helft, and John Regehr contributed one way or the other to the technical content of these posts. The work itself was funded by the DGA RAPID project ASECFLOD.
