dslab-epfl / klint Goto Github PK

View Code? Open in Web Editor NEW

8.0 8.0 5.0 2.36 MB

Repository for the "Automated Verification of Network Function Binaries" paper (NSDI'22).

License: MIT License

Lua 4.79% Shell 2.25% C 10.97% Python 79.06% Nextflow 0.33% Makefile 0.76% Rust 1.84%

klint's People

Stargazers

Watchers

Forkers

kylerky sdsen palanik1 c4dt kyechou

klint's Issues

Cleaner contracts

@tharvik this is a quick example of what I meant in our discussion yesterday as what index_pool's contract could look like instead of the current angr-dependent mess:

from klint import assume, any_bool, any_int, Map, sizeof
from klint.types import size_t, time_t, TIME_MAX, SIZE_MAX

# ideally we'd be able to use "not", "and", "or" but that requires patching the Python interpreter so... probably not
# instead, ~, &, | it is...

# I wonder if those doc comments are even needed? perhaps only optionally for the names of the function
# if they don't follow some convention (like struct_name_method_name), the parameters can probably be inferred?

class IndexPool:
    def __init__(self, size, expiration_time):
        """struct index_pool* index_pool_alloc(size_t size, time_t expiration_time)"""
        assert(size * sizeof(time_t) <= SIZE_MAX)
        self.size = size
        self.expiration_time = expiration_time
        self.items = Map(size_t, time_t)

    def borrow(self, time):
        """bool index_pool_borrow(struct index_pool* pool, time_t time, size_t* out_index, bool* out_used)"""
        assert(time != TIME_MAX)
        result = any_bool()
        index = any_int()
        used = any_bool()
        if self.items.length() == self.size:
            if self.items.forall(lambda k, v: time < self.expiration_time | (time - self.expiration_time) <= v):
                assume(~result)
            else:
                assume(result)
                assume(used)
        else:
             assume(result)
        if result:
            assume(index < self.size)
            if used:
                assume(self.items.contains(index))
                assume(time >= self.expiration_time)
                assume((time - self.expiration_time) > self.items.get(index))
            else:
                assume(~self.items.contains(index))
            self.items.set(index, time)
        return (result, index, used)

    def refresh(self, time, index):
        """void index_pool_refresh(struct index_pool* pool, time_t time, size_t index)"""
        assert(time != TIME_MAX)
        assert(index < self.size)
        self.items.set(index, time)

    def used(self, time, index):
        """"bool index_pool_used(struct index_pool* pool, time_t time, size_t index)"""
        value = self.items.get(index)
        if value is None:
            return False
        else:
            return time < self.expiration_time | (time - self.expiration_time) <= value

    def return(self, index):
        """void index_pool_return(struct index_pool* pool, size_t index)"""
        assert(index < self.size)
        self.items.remove(index)

Obviously just an example, I'm not even 100% sure it has all of the info necessary and only that, but I thought it'd be useful to write a clean version since the angr-specific one is a bit of a pain to understand.

`make verify-iptables_blacklist` raise `AssertionError: The rule should no longer be in the map`

currently, verifying the iptables_blacklist NF doesn't work.

from what I gathered, it is the only spec where a branch is actually "Multivalued!".
the assertion is actually sent by the spec, meaning in my understanding that the selected branch can't be taken.
but in tool/klint/verif/symbex.py:_symbex, it actually try for a "choice" exception but not for a "bad branching" exception. maybe the constraints are too loose and this path shouldn't happen?

Can't create the venv any more

solal@blue:~/klint$ make verify-nop
python3 -m venv /home/solal/klint/tool/venv
touch /home/solal/klint/tool/venv/.venv-created
. /home/solal/klint/tool/venv/bin/activate && \
        pip install /home/solal/klint/tool
Processing ./tool
  Installing build dependencies ... done
  Getting requirements to build wheel ... error
  ERROR: Command errored out with exit status 1:
   command: /home/solal/klint/tool/venv/bin/python3 /tmp/tmp1z20lyvd get_requires_for_build_wheel /tmp/tmpjba7y6pd
       cwd: /tmp/pip-req-build-opds1t5h
  Complete output (35 lines):
  Traceback (most recent call last):
    File "/tmp/tmp1z20lyvd", line 280, in <module>
      main()
    File "/tmp/tmp1z20lyvd", line 263, in main
      json_out['return_val'] = hook(**hook_input['kwargs'])
    File "/tmp/tmp1z20lyvd", line 114, in get_requires_for_build_wheel
      return hook(config_settings)
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/build_meta.py", line 338, in get_requires_for_build_wheel
      return self._get_build_requires(config_settings, requirements=['wheel'])
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/build_meta.py", line 320, in _get_build_requires
      self.run_setup()
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/build_meta.py", line 335, in run_setup
      exec(code, locals())
    File "<string>", line 1, in <module>
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/__init__.py", line 108, in setup
      return distutils.core.setup(**attrs)
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/_distutils/core.py", line 147, in setup
      _setup_distribution = dist = klass(attrs)
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/dist.py", line 475, in __init__
      _Distribution.__init__(
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/_distutils/dist.py", line 283, in __init__
      self.finalize_options()
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools/dist.py", line 904, in finalize_options
      ep(self)
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools_scm/integration.py", line 127, in infer_version
      _assign_version(dist, config)
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools_scm/integration.py", line 63, in _assign_version
      _version_missing(config)
    File "/tmp/pip-build-env-wi944sv2/overlay/lib/python3.8/site-packages/setuptools_scm/__init__.py", line 108, in _version_missing
      raise LookupError(
  LookupError: setuptools-scm was unable to detect version for /tmp.

  Make sure you're either building from a fully intact git repository or PyPI tarballs. Most other sources (such as GitHub's tarballs, a git checkout without the .git folder) don't contain the necessary metadata and will not work.

  For example, if you're using pip, instead of https://github.com/user/proj/archive/master.zip use git+https://github.com/user/proj.git#egg=proj
  ----------------------------------------
ERROR: Command errored out with exit status 1: /home/solal/klint/tool/venv/bin/python3 /tmp/tmp1z20lyvd get_requires_for_build_wheel /tmp/tmpjba7y6pd Check the logs for full command output.
make: *** [Makefile:30: /home/solal/klint/tool/venv/.env-done] Error 1

@tharvik does your fancy venv creation have some requirements beyond just having Python installed? It first asked me to get python3.8-venv on apt, which I did, and now it outputs this. And /tmp is completely empty so no logs or files I can inspect.

`make verify-dns_aaa_records` raise `Exception: Cannot borrow from an ephemeral allocation`

when trying to verify nf/dns_aaa_records, it raises this weird exception.
looking at the readme, its status is "Not verified". shall I also remove it in the coming up PR deleting the paper related files?
or is it indeed a bug that should be addressed?

Proper BPF support?

@tharvik in case that's in line with the C4DT's priorities, having Klint work on BPF programs directly (not the hacky stuff from the paper) might be a good showcase.

A student had almost finished BPF ISA support for angr in a semester project with me, but some issues cropped up in the actual PR and I guess there wasn't time after the semester to finish it. Maybe it can be resurrected? angr/angr-platforms#46

dslab-epfl / klint Goto Github PK

klint's People

Stargazers

Watchers

Forkers

klint's Issues

Cleaner contracts

`make verify-iptables_blacklist` raise `AssertionError: The rule should no longer be in the map`

Can't create the venv any more

`make verify-dns_aaa_records` raise `Exception: Cannot borrow from an ephemeral allocation`

Proper BPF support?

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent