Newer
Older
---
layout: post
author: Pascal Cuoq
date: 2011-01-13 22:01 +0200
categories: value
format: xhtml
title: "Why don't you verify the entire Internet ?"
summary:
---
{% raw %}
<p>... or at least the C codebase available on there, anyway?</p>
<p>Don't be fooled by the positive examples presented here and there. Verifying arbitrary programs is still arbitrarily difficult. There is some cherry-picking going on in the results we, and others, present.</p>
<p>In the case of Frama-C's value analysis, dynamic allocation is one issue. This analysis was never intended to analyze programs that use it. I wonder if it would be possible to get interesting results by modelizing the heap as a single large array whose contents are voluntarily kept imprecise. But I never tried, if that tells you how optimistic I am.</p>
<blockquote><p>Aside: this is purely a limitation of the value analysis plug-in, not of the framework. See for instance <a href="http://www.liafa.jussieu.fr/~sighirea/celia/examples.html" hreflang="en">this plug-in</a> for an attempt that we are eager to hear more about to handle C programs with dynamic allocation.</p>
</blockquote>
<p>Surprisingly often though the reason I do not start a new experiment is not that Frama-C's value analysis couldn't handle the source code but that I couldn't. Functional C code is often ugly — for reasons that given the language and the objectives are unavoidable. The program tries to work as a shared library; it want to compile on 1995's version of DJGPP for MS-DOS; ...</p>
<p>Yesterday at 17:00 I was discovering another gem of simple and efficient code comparable in cleanliness to Skein. And not to boast or anything simply as a measure of how efficient one can be when equipped with the right tool today at the same time I was reporting a tiny flaw in said library that has since been semi-acknowledged by its author.</p>
<p>I'd start a new thread but I haven't finished presenting the analysis of Skein.</p>
{% endraw %}