[klee-dev] Dockerizing Klee

Pablo González de Aledo pablo.aledo at gmail.com
Thu Feb 26 18:06:20 GMT 2015


Is there any benefit on using Docker over CDE?. As far as I know CDE is
open-source and was developed by a guy who worked in klee at some stages
(less relevant, but nice to know :-P).

Regards.

2015-02-26 18:58 GMT+01:00 Cristian Cadar <c.cadar at imperial.ac.uk>:

> 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
>>
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list