[klee-dev] Dockerizing Klee

[Cristian Cadar]

Hi guys,

That's great, thanks for sharing this with the list.  I think Docker is 
a nice medium for distributing KLEE, and in fact there were several 
other people who have "dockerized" KLEE recently:
https://github.com/riyadparvez/klee-docker
https://registry.hub.docker.com/u/petrhosek/klee/
https://registry.hub.docker.com/u/oscarsd/klee-release/
https://registry.hub.docker.com/u/kleeweb/klee/
https://registry.hub.docker.com/u/mbrt/klee/
etc.

I think it would be useful to have an official repository for the 
dockerized KLEE, which we would recommend to new users on the KLEE 
website, and which would be maintained as part of the KLEE project on 
GitHub (https://github.com/klee).  Also, it would be useful to 
automatically update an associated KLEE Docker image and upload it to 
the Docker registry either after each KLEE commit, or at regular time 
intervals.

These are just my initial thought though, and it would be useful to get 
other opinions.

Best,
Cristian


On 26/02/15 16:14, Makula, Szymon wrote:
> Hello All,
>
> Docker is a relatively recent technology that developers and sysadmins
> use to build, ship, and run distributed applications. Compared to
> virtual machines, docker is more lightweight and efficient, since it
> provides an additional layer of abstraction of operating-system-level
> virtualization. You can read more about it at https://www.docker.com/.
>
> The use of docker makes Klee much easier to deploy and get started with.
> We have dockerized Klee and you can find the result of our labors at
> https://github.com/szymoniks/Klee-Docker.
>
> To install docker, please follow the guide at
> https://docs.docker.com/installation/#installation. After the
> installation and cloning our project, you can simply execute the
> following command from the project root directory to build Klee:
>
> $sudo docker build -t [image_name] .
>
> Where image_name can be any name for the final image one fancies! :) By
> default, the number of jobs for make commands is 5, which one can change
> it in Dockerfile to adjust for their machine’s specification. We address
> the security concerns of sudo-ing this script below.
>
> This command builds Klee, following the instruction in the guide on
> http://klee.github.io/getting-started/as of 26/02/2015. The image is
> based on an official Ubuntu 14.04 docker image and will be supplied with
> LLVM-GCC 2.9, LLVM 2.9, STP r940 and uclibc (provided by Klee community
> at https://github.com/klee/klee-uclibc.git).
>
> To work in the virtualized environment where Klee is installed, type the
> command:
>
> $sudo docker run -t -i [image_name] /bin/bash
>
> Again, we address the security concerns of sudo-ing this script below.
>
> We used the following options:
>
> ·-i : keep STDIN open even if not attached
>
> ·-t : allocate a pseudo-TTY
>
> For more information, please read README or check
> https://docs.docker.com/reference/commandline/cli/.
>
> Please feel free to contact us with any questions.
>
> Best regards,
>
> Szymon Makula and Zheng Gao
>
> University College London
>
> *Security*
>
> Docker has been used and trusted by different companies, such as Gilt
> Groupe Inc., Yelp, and Baidu Inc, so we believe it does not contain any
> trojans or malware.
>
> We have used Docker version 1.2.0 and Klee is built on Ubuntu 14.04.
>
> The docker daemon always runs as the root user, and since Docker version
> 0.5.2, the docker daemon binds to a Unix socket instead of a TCP port.
> By default that Unix socket is owned by the user root, and so, by
> default, you need to access it with sudo.
>
> Starting in version 0.5.3, if you (or your Docker installer) create a
> Unix group called docker and add users to it, then the docker daemon
> will make the ownership of the Unix socket read/writable by the docker
> group when the daemon starts. The docker daemon must always run as the
> root user, but if you run the docker client as a user in the docker
> group then you don't need to add sudo to all the client commands. As of
> 0.9.0, you can specify that a group other than docker should own the
> Unix socket with the -G option. However, the docker group (or the group
> specified with -G) is root-equivalent.
>
> You can verify that the script does nothing more by inspection. The
> secure hash of the Dockerfile and two patches can be found in the
> checksum file.
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>