Last week, security researcher lcamtuf blogged about CVE-2014-8485, a vulnerability in the Unix
strings command. The
strings command is a popular way to get hints when stuck in the venerable ADVENT game. Some may also use it to reveal sequences of printable characters other than the verbs in ADVENT, but the truth is that running
strings on a modern binary file is a depressing experience. On my computer,
strings `which frama-c` shows that the 15MiB binary contains 111 copies of the string “volatile”, 53 copies of the identifier name “vlogic_ctor_info_decl”, and two copies of “verify_unmodified: %s has conflicting definitions. cur: %a”, a debug message not intended to ever be seen by the user. And I am only going through the Vs!
In fact, the entire Turbo Pascal compiler could probably fit in the space occupied by useless messages that start with “V” in Frama-C:
$ strings `which frama-c` | grep ^[vV] | wc
3638 4788 46623
Coming back to the vulnerability, it came as a shock to Unix users—unfortunately that vulnerability name was already taken. The purpose and function of the
strings command is to scan binary files of unknown origin and/or mysterious design, and suddenly lcamtuf tells us that doing so could lead to arbitrary code execution!
This has prompted a series of very short implementations of the basic functionality that
strings is supposed to provide, in Python and in C. Depressing references to the evolution of the sizes of binaries notwithstanding, there is no reason for
strings to be written in C, except perhaps if you anticipate that you will need to run it from a boot disk. Python seems, on the face of it, like an excellent choice. Java or OCaml would also have been reasonable. Regardless, Twitter user nils offered at one point the C implementation below:
And at another point, athoshun proposed the shorter:
These two definitions are remarkably concise; they both rely on the same trick of moving some of the responsibility onto the terminal by clever use of the “carriage return” character 13 in ASCII. This means that these implementations fool the user into thinking that they work, but the illusion doesn't hold when the output is not directly interpreted by a terminal:
$ ./a.out < a.out
$ ./a.out < a.out | more
Ignoring the non-standard prototype for
main and the concise declarations
c; that are par for the C code golf course, the versions above are remarkable in that they both invoke undefined behavior in line 1:
warning: undefined multiple accesses in expression. assert \separated(&a, &a);
This is just a blip caused by the race to conciseness. The expression
a<4|(a=0)?13:10 is intended as a shorter alternative to
a<4||(a=0)?13:10, but unfortunately,
| does not introduce the sequence point that is needed between the assignment
a=0 and the use
a<4. The situation is similar with
(6>a)*3+9+(a=1) in the second implementation.
Other versions of
strings, written by the same authors, that do not suffer from the unsequenced-side-effects undefined behavior, are:
Are these safe? We need a specification for
getchar() to find out:
/*@ ensures -1 ≤ \result ≤ 255 ; */
Without this specification, it looks like
c+1 in the first implementation might be a signed arithmetic overflow (which is undefined behavior). With the specification, it is clear that it isn't, since
c is initially 0 and then the result of
getchar(), which is at most 255.
Once the specification is provided:
$ tis-analyzer good_string1.c
warning: signed overflow. assert a+1 ≤ 2147483647;
$ tis-analyzer good_string2.c
The first implementation still has a slight issue: tis-analyzer is unable to demonstrate that, with the information provided, the variable
a does not eventually overflow. Looking at the code, we can see that this can only happen for sequences of printable characters longer than 231 characters. A simple way to ensure that it doesn't is not to trust the outside world with files larger than 2GiB.
The second implementation is free of undefined behavior for as many characters as you want to feed it. Since the functionality it intentionally provides is not the remote execution of arbitrary code, you can pass any sequence of character to it confident in the knowledge that it will not accidentally provide this functionality through undefined behavior to the malicious author of a perplexing file. Consider this implementation recommended. In fact, I'll run it on
frama-c right now:
$ ./a.out < `which frama-c`
… oh, no!
In conclusion, much of the software around us seems to be too complex for its own good: OpenSSL, Bash, strings, … but we do not have to use the complex versions. Simpler implementations of just the right functionality are also available or can be written—though aiming for less than 80 characters is a bit extreme. It is easier to trust that the simpler versions do what you want and only what you want. When necessary, the simpler implementations can be formally verified to reach greater yet levels of confidence.