klee / klee-web

KLEE in the browser

KLEE Symbolic Virtual Machine

KLEE is a symbolic virtual machine built on top of the LLVM compiler infrastructure. Currently, there are two primary components:

1. The core symbolic virtual machine engine; this is responsible for executing LLVM bitcode modules with support for symbolic values. This is comprised of the code in lib/.

2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with additional support for making parts of the operating system environment symbolic.

Additionally, there is a simple library for replaying computed inputs on native code (for closed programs). There is also a more complicated infrastructure for replaying the inputs generated for the POSIX/Linux emulation layer, which handles running native programs in an environment that matches a computed test input, including setting up files, pipes, environment variables, and passing command line arguments.

For further information, see the webpage.

klee-web's Issues

GeoLite2 databases are no longer served publicly

I was having troubles setting up development environment according to instructions. Looks like docker build is failing:

Step 11/14 : RUN DEVELOPMENT=1 ./build.sh
 ---> Running in 99154dd3cf30
Running flake8
Downloading GeoIP
Removing intermediate container 99154dd3cf30

I tracked it down to these lines:

klee-web/src/klee_web/build.sh

Lines 12 to 13 in e5cab8c

	wget -q -P "${CUR_DIR}/geoip" https://geolite.maxmind.com/download/geoip/database/GeoLite2-City.mmdb.gz
	wget -q -P "${CUR_DIR}/geoip" https://geolite.maxmind.com/download/geoip/database/GeoLite2-Country.mmdb.gz

And here is a likely reason:

On December 30, 2019, downloads will no longer be served from our public GeoLite2 page, from geolite.maxmind.com/download/geoip/database/*, or from any other public URL.

To continue using GeoLite2 databases:

1. Review our new GeoLite2 EULA.
2. Sign up for a MaxMind account.

Split repository into public and private parts

The idea is to keep all the public code necessary to run klee-web locally in the public repository, but move all private deployment data (passwords, etc.) into a private repository. This would address #63 .

Rework git_repo group_var

Swap this variable to the canonical repo here.

angstwad.docker_ubuntu does not install docker-py

Vagrant up fails on TASK redis : Docker pull Redis 3.2

The problem seems to be a missing installation of docker-py. Maybe investigate to find another plug-in to install docker.

Update Node.js into latest version

Look here

Move circleci to 2.0

Fix /manage

The manage page does not have correct data for the tasks

Symbolic arguments not working

Enabling symbolic arguments does not work. This can be observed by enabling symbolic arguments and then looking at the "Ran command" message displayed on the right window, which does not show "--sym-args" being passed to KLEE.

`vault_password_file` problem

Hello, I'm a student who wants to learn from klee-web project.
I followed the guide: Getting started on development in README.md file
I have installed VirtualBox, Vagrant, and Ansible by apt-get.(I'm using Ubuntu14.04)
When I started the development virtual machine with the command: vagrant up.
I catched these error infomations:

There are errors in the configuration of this machine. Please fix
the following errors and try again:

ansible provisioner:
* `vault_password_file` for the Ansible provisioner does not exist on the host system: /home/MyUserName/.klee_vault_password

It's may depended on the config in Vagrantfile

  config.vm.provision "ansible" do |ansible|
    ansible.playbook = "provisioning/vagrant.yml"
    ansible.verbose = "vvvv"
    ansible.vault_password_file = "~/.klee_vault_password"
  end

I'm a rookie programmer, so I don't know how to solve this problem.
Would you please give me some advice?

Best regards.

Hidden Examples and Tutorials when logged in

Let the examples and tutorials be visible to the user who is logged in.

Can't pass multiple options?

Trying to pass -posix-runtime -search=bfs -max-depth=10 as options results in:

Error running /home/klee/klee_build/bin/klee -posix-runtime -search=bfs -max-depth=10 /tmp/code/code.o:
klee: Unknown command line argument '-posix-runtime -search=bfs -max-depth=10'.  Try: '/home/klee/klee_build/bin/klee -help'
klee: Did you mean '-posix-runtime=bfs -max-depth=10'?

It seems like the string is being passed as a single argument to klee, even if it contains spaces.

Restart Worker when Celery fails

There seems to be an issue with celery that the worker stops listening to request if a celery heartbeat is missed.
These are some threats that I found where people seemed to have similar issues:
celery/celery#4997
celery/celery#4185
analyseether/ether_sql#42
celery/celery#2296

Right now, there is a cronjob that checks every hour if the worker's log shows a missed heartbeat and restarts the container in that case. This works fine for now, but there might be more elegant solutions for the future.

KLEE Web Error Running clang on vanilla example

Prob. should have posted here.
klee/klee#1345

Fix end-to-end Klee Web tests on CircleCI

The end-to-end test for Klee Web seem to fail on CircleCI.
Investigate and solve this issue.

Fix the Klee Web coverage report.

This issue is due to klee/klee#461.

Freeze all dependences

The projects we depend on are constantly evolving and introduce breaking changes. I'll try to create a exhaustive list of all dependences that needs to be frozen. Ideally we should have a "single source of truth" that we explicitly declare all versions of every dependency. This file should be read by ansible which should generate the needed templates.

Dependences:

• KLEE Docker image
• Django dependences
• Node.JS dependences
• Frameworks (Django, PhandomJS, etc)

Enable downloading raw KLEE results in development mode

Right now, trying to download KLEE's raw results in development mode is not possible.

Use REST practices for /job/notify

Change how you use channel. Replace it with task_id.

Public web-hosted instance (http://klee.doc.ic.ac.uk) returns "502 Bad Gateway"

I don't know if the issue is temporary or persistent, but either it should be fixed or the link should be removed from README and website.

Add C++ support

I've tried to enter the following code:

class Foo {};

int main()
{
  return 0;
}

... and I'm getting:

Error running /usr/bin/clang-6.0 -I /home/klee/klee_src/include -emit-llvm -c -g /tmp/code/code.c -o /tmp/code/code.o:
/tmp/code/code.c:1:1: error: unknown type name 'class'
class Foo {};
^
/tmp/code/code.c:1:10: error: expected ';' after top level declarator
class Foo {};
         ^
         ;
2 errors generated.

Please add an option to select C++ compiler.

klee-output S3 bucket

The klee-output S3 bucket that's used by klee-web is on my personal AWS S3 account. I'm planning on deleting the bucket in 1 week if no-one responds, at which time it'll be free for anyone else with an AWS account to claim.

If you'd like to keep that specific bucket reply on the thread and we can arrange a time for me to delete the bucket to ensure the best chance of keeping the name.

move to gitlab?

Display bug in the /manage interface

The labels in the bar chart shown in the /manage interface are not displayed correctly when there is a large number of jobs in one of the days.

Pass `receivers_email` as an ENV variable

Currently receivers_email is hardcoded into the source code. Pass receivers_email as an ENV variable here with Ansible for better flexibility.