Blog

Arithmetic overflows in Fluorine
Pascal Cuoq on 9 July 2013

There is a C quiz in the middle of this post, lost in the middle of all the reminiscing. A history of arithmetic overflows in Frama-C From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows...

Read More

On the precise analysis of C programs for FLT_EVAL_METHOD==2
Pascal Cuoq on 6 July 2013

There has been talk recently amongst my colleagues of Frama-C-wide support for compilation platforms that define FLT_EVAL_METHOD as 2. Remember that this compiler-set value, introduced in C99, means that all floating-point computations in the C program are made with long double precision, even if the type of the expressions they...

Read More

On the prototype of recv()
Pascal Cuoq on 20 June 2013

Typing man recv on my system, I get: ssize_t recv(int socket, void *buffer, size_t length, int flags); The man page contains this additional bit of specification: “These calls return the number of bytes received, or -1 if an error occurred.” The type ssize_t is defined as a signed variant of...

Read More

Microsoft's bug bounty program
Pascal Cuoq on 19 June 2013

I like Robert Graham's analysis on Microsoft's new bug bounty program. I would never have thought of selling vulnerabilities to the NSA (but then I am not American and not a security researcher). Does the NSA not employ qualified people to look for vulnerabilities as their day job? Is that...

Read More

Attack by Compiler
Pascal Cuoq on 20 May 2013

The title of this post, “Attack by Compiler”, has been at the back of my mind for several weeks. It started with a comment by jduck on a post earlier this year. The post's topic, the practical undefinedness of reading from uninitialized memory, and jduck's comment, awakened memories from a...

Read More