[klee-dev] Dockerizing Klee

Thu Feb 26 18:30:55 GMT 2015

Yes, there are several, e.g., it's more general than CDE, which makes no 
guarantees about the ability to exercise new behaviours of the software 
being packaged; it is actively maintained (also as open-source); and it 
hosts a public registry which makes distribution easier.

Of course, I'm happy to see the CDE packaged up-to-date, and I opened a 
pull request about this in 2013 
(https://github.com/klee/klee/issues/42), but nobody took up the job, 
and the discussion veered instead toward Docker.

Cristian

On 26/02/15 18:06, Pablo González de Aledo wrote:
> 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
> <mailto: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://github.com/riyadparvez/klee-docker>
>     https://registry.hub.docker.__com/u/petrhosek/klee/
>     <https://registry.hub.docker.com/u/petrhosek/klee/>
>     https://registry.hub.docker.__com/u/oscarsd/klee-release/
>     <https://registry.hub.docker.com/u/oscarsd/klee-release/>
>     https://registry.hub.docker.__com/u/kleeweb/klee/
>     <https://registry.hub.docker.com/u/kleeweb/klee/>
>     https://registry.hub.docker.__com/u/mbrt/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
>         <https://github.com/szymoniks/Klee-Docker>.
>
>         To install docker, please follow the guide at
>         https://docs.docker.com/__installation/#installation
>         <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
>         <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
>         <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/
>         <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 <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>         <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>     _________________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>     <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
>