From Facebook to Silent Circle, through the “metrics” Frama-C plug-in
Pascal Cuoq - 16th Feb 2013From Facebook to Silent Circle
Some computers at Facebook were recently compromised because of a zero-day in Java. Nothing unexpected. Last december instead of writing a full blog post I lazily linked to Robert Graham predicting this sort of thing for the year 2013.
Speaking of Facebook do you know who cares for your privacy? The good people at Silent Circle. They provide end-to-end encryption to use on your mobile phone so that the only people to hear your discussions with your loved ones or business partners are you and them and perhaps passengers in the same compartment as you if you are this sort of sociopath.
Speaking of Robert Graham he has written another excellent post on the dangers of only focusing on the obviously important the hard-to-get-right but known-to-be-hard-to-get-right cryptographic stuff and neglecting the mundane such as parsing. He takes the example of source code recently released by Silent Circle finding traces of amateurism in the implementation of SDP. This is not were the hard cryptographic stuff takes place. But because this is a C++ implementation any exploitable flaw at this level could have deep security implications. A buffer overflow could result in execution of code chosen by the attacker and the attacker-chosen code could disable the cryptography entirely or worse.
An attack on the protocol implementation is the equivalent of a $5 wrench in a well-known cryptography-related XKCD comic that probably does not require linking to at this point.
A mysterious commit message
[Metrics] Fix most complicated plugin ever metrics (globals counted twice if declared and defined)
The above is the message attached by a facetious colleague to commit 21435 during the just elapsed week. After inquiry the message is at least one-third sarcastic. Still no-one ever said that the metrics plug-in should be simpler or easier to get right on first try than any of the other Frama-C plug-ins. And in fact this was neither the first nor the last minor issue fixed in that plug-in last week.
Frama-C's metrics plug-in gathers various measurements of a syntactic nature. The “metrics” plug-in can help check how much of an unfamiliar codebase has actually been analyzed with a plug-in of a more semantic flavor such as the value analysis. It is used in context in the next section of this post.
One reason “metrics” as hard to get right as any other Frama-C plug-in is that it deals with syntax. Semantic plug-ins such as the value analysis only need manipulate abstract objects such as functions and variables. In the metrics plug-in details matter such as the nuance between the declaration (in a .h header file) and the definition (in a .c file) of the same function (that was the bug being fixed in commit 21435) or the subtle difference between the source location of a variable and the source location of its initializer (that was another bug fixed this week).
Metaphorically the metrics plug-in is to the Frama-C platform what the SDP parser is to an end-to-end encryption solution. It is not sexy but it is just as hard to get right and as essential as the rest.
Using the metrics plug-in
Life being what it is we sometimes find ourselves analyzing very unfamiliar code. I am talking code without documentation here and often without either the hardware or a minimal description of the hardware that would be necessary to understand what behaviors can be exercised in the source code. This is one case when the metrics plug-in helps either anticipate how much work will be necessary or how much has already been done.
Inspired by Robert Graham's post I converted the Silent Circle SDP parser from C++ to C so as to see whether I could not find a bug in it using Frama-C's value analysis. At some point I had this modified parseSDP.c file and this modified sdp.h file. The originals can be seen here for parseSDP.c and sdp.h.
$ frama-c -cpp-command "gcc -C -E -I. -I `frama-c -print-share-path`/libc" parseSDP.c -metrics
[kernel] preprocessing with "gcc -C -E -I. -I /usr/local/share/frama-c/libc parseSDP.c"
parseSDP.c:120:[kernel] warning: Calling undeclared function ipstr2long. Old style K&R code?
parseSDP.c:121:[kernel] warning: Calling undeclared function reverseIP. Old style K&R code?
parseSDP.c:328:[kernel] warning: Calling undeclared function u. Old style K&R code?
[metrics] Defined functions (6)
=====================
findMediaId (0 call); hasAttrib (0 call); findCrLf (4 calls);
findip (3 calls); getMediaParams (1 call); parseSDP (0 call);
Undefined functions (10)
========================
printf (1 call); strlen (1 call); strncmp (6 calls); atoi (2 calls);
isdigit (4 calls); islower (1 call); isxdigit (1 call); ipstr2long (1 call);
reverseIP (1 call); u (4 calls);
Potential entry points (3)
==========================
findMediaId; hasAttrib; parseSDP;
...
This snapshot arrives at a good time to use the metric plug-in as above. The plug-in says that good entry points to start the analysis from are findMediaId() hasAttrib() and parseSDP(). The heuristic here is that these functions are provided and aren't called so they are likely to be part of the API.
The metrics plug-in also says that the only missing functions are those from printf() to isxdigit() (these are part of the standard library) u() (I introduced this function myself when converting from C++ to C) and ipstr2long() and reverseIP() that are the only two that require digging up from elsewhere in the codebase. At that point I decided that the functions probably weren't important and that I could let Frama-C infer some sort of behavior for them based on their respective types.
The $5-wrench kind of flaw in the verification process would be to fail to notice that an important function is missing. Then the value analysis might report few or no issues not because the code is safe but because the analysis failed to visit most of it. In another scenario the value analysis might fail to visit a large part of the code because there is an error early on that makes it look like the rest is unreachable. The “metrics” plug-in is the best safeguard we have against this kind of mistake which is easy to make when verifying unfamiliar code.
A quick look at function parseSDP()
I finally used the commandline:
$ frama-c -cpp-command "gcc -C -E -I. -I `frama-c -print-share-path`/libc" parseSDP.c \
-lib-entry -main parseSDP -context-valid-pointers -context-width 20 -val
Here are a few alarms found this way cherry-picked as interesting because they are caused directly from the contents of the buffer pointed to by buf that we assume to be under an attacker's control for this exercise.
Some alarms seem by contrast to be caused by the contents of
*psdp. These are not as interesting to investigate because that structure probably has some invariants it is supposed to satisfy so the alarms we get there are only caused by the lack of context.
From the way it is handled inside parseSDP() it seems that buf is only assumed to point to a zero-terminated string. It is a good way to pass a Sunday afternoon to see whether these alarms correspond to a real danger of buffer overflow for some input.
parseSDP.c:84:[kernel] warning: out of bounds read. assert \valid_read(buf+1); parseSDP.c:82:[kernel] warning: out of bounds read. assert \valid_read(buf); ... parseSDP.c:162:[kernel] warning: out of bounds read. assert \valid_read(buf); parseSDP.c:165:[kernel] warning: out of bounds read. assert \valid_read(buf-2); parseSDP.c:167:[kernel] warning: out of bounds read. assert \valid_read(buf+1); ... parseSDP.c:262:[kernel] warning: out of bounds read. assert \valid_read(buf); ... parseSDP.c:291:[kernel] warning: out of bounds read. assert \valid_read(buf); parseSDP.c:294:[kernel] warning: out of bounds read. assert \valid_read(buf); ... parseSDP.c:300:[kernel] warning: out of bounds read. assert \valid_read(buf); ... parseSDP.c:303:[kernel] warning: out of bounds read. assert \valid_read(buf); ... parseSDP.c:308:[kernel] warning: out of bounds read. assert \valid_read(buf); ... parseSDP.c:308:[kernel] warning: out of bounds read. assert \valid_read(buf); parseSDP.c:309:[kernel] warning: out of bounds read. assert \valid_read(buf);