We present a language agnostic approach for the dynamic and static checking of .NET assemblies. Dynamic checking is obtained through Foxtrot, which allows specifying contracts in a language independent way. Contracts are made persistent by compiling them into pure MSIL. Runtime contract checking, including contract inheritance is achieved via binary rewriting. Language agnostic static checking is achieved though Clousot, which is an abstract intepretation-based static analyzer for the analysis of .NET assemblies. It contains abstract domains for checking out-of-bounds array accesses, null dereferences, string usage, and memory accesses in unsafe managed code. It can statically validate Foxtrot contracts. We have tested Clousot on all the assemblies of the .NET framework.

Details