Information Flow analysis in VCC

Editor
May 25, 2010 at 2:14 PM

Hi all,

My latest commit introduces basic support for information flow properties in VCC. At the moment, only local variables of primitive type are supported (heapified or not), and we have no way of specifying information-flow properties in function contracts.
The new test file vcc2\informationFlow contains a few very simple examples, showing the basic syntax for the currently supported information flow properties and annotations. You can ask VCC to prove that an expression has a low level (at the moment, only a variable or a pointer dereference where the pointer is a variable) using the is_low() predicate, and specify if a test condition has to be evaluated as being high or low using the test_classifier(classifier,condition) in place of the test condition, where classifier is an arbitrary boolean expression (if it evaluates to true, then the test and the branching will be evaluated in a high context, otherwise, an assertion enforces that the condition is indeed low and the the branching will be evaluated in a low context).

I am of course interested in your feedback on those first few things. Of special interest to me are:

  • soundness issues,
  • and error reporting improvements.

I am aware of a few places where the precision of the analysis could be improved, but I am of course interested in getting your feedback on that point as well. Please, also let me know if anything else is broken by my modifications. I put in place a mechanism to prevent the generation of the information-flow VCs in the absence of information-flow annotations, but there ay be bugs hiding away in there too.

Cheers,
Francois

Coordinator
May 26, 2010 at 7:59 PM

Hi Francois,

  with the vcc9.sln build (i.e. for VS version prior to VS 2010) I now get a build error:

    vcc\Host\VccPlugin.cs(456,5): error CS0246: The type or namespace name 'HashSet' could not be found (are you missing a using directive or an assembly reference?)

  Maybe older VS version do not provide HashSets?

  Best, Mark

Editor
May 26, 2010 at 8:33 PM
Edited May 27, 2010 at 12:08 PM

Thanks Mark.

Stephan and I went through my code and identified a number of other things I may have broken on the C# bits of the code without breaking the build server's cycle. I'll upload a fix first thing tomorrow morning (my internet connection at home is a tad slow).
In the long run, the dirty hacks I added in there are probably going to disappear and we will be reporting under-specifications as errors instead of letting them slide.
Francois
Editor
May 27, 2010 at 12:10 PM

Hi Mark.

This is now fixed (and I checked that the whole thing compiled with VS 2008). Sorry for the time it took, I had to track down a data structure that would do approximately the same thing but be provided by both versions of .NET, and that was less easy than it seemed.
Anyhow, thanks again for the heads up.

Francois

Coordinator
May 27, 2010 at 12:30 PM

Thanks Francois, indeed it builds for us / me as well!

Mark

Nov 7, 2014 at 7:08 PM
Hi all,

could someone tell me please what is the current status on information flow analysis with VCC? I would need to implement a taint analysis ensuring that some secret values may not influence anything leaving the program but when using a specified interface. Is that possible?

Best, Max
Editor
Nov 8, 2014 at 7:19 PM
Hi Max,

The information-flow analysis did not survive improvements to the tool. It's possible that some of the code is left in the current code base. Depending on the complexity of the programs and properties you are interested in proving, you might be able to plug things back in pretty quickly.

Cheers,
Francois