CodeHawk static analysis tool suite

[roberth]

Project description

The CodeHawk Tool Suite, originally developed by Kestrel Technology, is a sound static analysis platform based on the mathematical theory of abstract interpretation developed by Patrick and Radhia Cousot. CodeHawk consists of a programming-language independent abstract interpretation engine and three language front ends [Java, C, x86]

Nixpkgs could use it to check its own C programs, such as the setuid wrappers and #124556.

For packaging it seems we'll need at least these repos:

https://github.com/static-analysis-engineering/codehawk https://github.com/static-analysis-engineering/CodeHawk-C

This is not about the JavaScript codehawk project, which seems to be entirely unrelated, despite performing performing some kind of analysis on JS.

Metadata

• homepage URL: http://kestreltechnology.com/technology.html
• source URL: https://github.com/static-analysis-engineering/codehawk
• license: mit
• platforms: unix, linux, darwin, ...

[bergkvist]

My setup so far

git clone https://github.com/static-analysis-engineering/CodeHawk-C
cd CodeHawk-C

I've added shell.nix to the CodeHawk-C folder with the following content:

# Use commit from https://github.com/NixOS/nixpkgs/pull/124556 to get access to pkgs.makeBinaryWrapper
{ pkgs ? import (fetchTarball "https://github.com/bergkvist/nixpkgs/archive/4b833cc141172f88e563692f2458253212d1cf1a.tar.gz") {} }:

let
  PROJECT_ROOT = toString ./.;
in pkgs.mkShell {
  buildInputs = [
    pkgs.gcc
    pkgs.python39
    pkgs.makeBinaryWrapper
  ];
  shellHook = ''
    export PYTHONPATH="${PROJECT_ROOT}"
    export PATH="${PROJECT_ROOT}/chc/cmdline/c_file/:$PATH"
  '';
}

nix-shell --pure
[nix-shell]$ mkdir -p wrapper-test && cd wrapper-test
[nix-shell]$ makeCWrapper /some/executable > main.c
[nix-shell]$ chc_parse_file.py main.c
[nix-shell]$ chc_analyze_file.py . main.c

But I get an exception from CodeHawk-C trying to analyze a simple C-file:

Traceback (most recent call last):
  File "/Users/tobias/repos/CodeHawk-C/chc/cmdline/c_file/chc_analyze_file.py", line 157, in <module>
    capp.collect_post_assumes()
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 351, in collect_post_assumes
    self.iter_files(lambda f: f.collect_post_assumes())
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 163, in iter_files
    f(file)
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 351, in <lambda>
    self.iter_files(lambda f: f.collect_post_assumes())
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 128, in collect_post_assumes
    self.iter_functions(lambda fn: fn.collect_post_assumes())
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 214, in iter_functions
    f(fn)
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 128, in <lambda>
    self.iter_functions(lambda fn: fn.collect_post_assumes())
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CFunction.py", line 203, in collect_post_assumes
    self.proofs.collect_post_assumes()
  File "/Users/tobias/repos/CodeHawk-C/chc/proof/CFunctionProofs.py", line 86, in collect_post_assumes
    self.spos.collect_post_assumes()
  File "/Users/tobias/repos/CodeHawk-C/chc/proof/CFunctionSPOs.py", line 68, in collect_post_assumes
    cs.collect_post_assumes()
  File "/Users/tobias/repos/CodeHawk-C/chc/proof/CFunctionCallsiteSPOs.py", line 299, in collect_post_assumes
    calleefun = cfile.capp.resolve_vid_function(cfile.index, self.callee.get_vid())
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 211, in resolve_vid_function
    return self.files[filename].get_function_by_index(tgtvid)
  File "/Users/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 202, in get_function_by_index
    raise Exception('Unable to find function with global vid ' + str(index))
Exception: Unable to find function with global vid 414

The file I'm trying to analyze (makeCWrapper /some/executable):

#include <unistd.h>
#include <stdlib.h>

int main(int argc, char **argv) {
    argv[0] = "/some/executable";
    return execv("/some/executable", argv);
}

[stale[bot]]

I marked this as stale due to inactivity. → More info