Frama-C A context-sensitive analysis Frama-C's value analysis is context-sensitive. This means that when a function f2() is called from a caller f1() function f2() is analyzed as many times as the analyzer goes over f1(). Function f2() is analyzed each time with a different program state—the program state corresponding to the...
Read MoreMy presentation Friday at the U3CAT meeting was on the topic of Frama-C Csmith testing. Several posts in this blog already describe facets of this work (it has its own tag). Yet another angle can be found in this short article draft. Said draft by the way will soon need...
Read MoreJustification There recently was a thread in the Frama-C mailing list on verifying the Rijndael cipher, standardized and better-known as AES. Nowadays, AES is mostly famous for being sensitive to timing attacks. An attacker measuring the time it takes to encrypt known plaintext with an unknown key can deduce the...
Read MoreExploring unfamiliar code Sometimes, one finds oneself in the situation of exploring unfamiliar code. In these circumstances, it is sometimes useful to know which functions a function f() uses. This sounds like something that can be computed from the callgraph, and there exists plenty of tools out there that can...
Read MoreHey, I left out one alarm last time: donut.c:15 ... out of bounds read. assert \valid(". -~:;=!*#$@"+tmp_7); This corresponds to ". -~:;=!*#$@"[N>0?N:0] in the obfuscated code. I wanted to have a blog post about this construct in particular because I was curious whether it would break the content management system's...
Read More