[klee-dev] Dockerizing Klee

Pablo González de Aledo pablo.aledo at gmail.com
Thu Feb 26 17:48:28 GMT 2015


I've seen klee "encapsulated" this way with CDE (a tool very similar to
Docker), several times before. However, it is good to see that installation
is getting easier :-)

2015-02-26 17:14 GMT+01:00 Makula, Szymon <szymon.makula.12 at ucl.ac.uk>:

>  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
>
>


-- 
_                                      =   (
                                        255,
                                      lambda
                               V       ,B,c
                             :c   and Y(V*V+B,B,  c
                               -1)if(abs(V)<6)else
               (              2+c-4*abs(V)**-0.4)/i
                 )  ;v,      x=1500,1000;C=range(v*x
                  );import  struct;P=struct.pack;M,\
            j  ='<QIIHHHH',open('M.bmp','wb').write
for X in j('BM'+P(M,v*x*3+26,26,12,v,x,1,24))or C:
            i  ,Y=_;j(P('BBB',*(lambda T:(T*80+T**9
                  *i-950*T  **99,T*70-880*T**18+701*
                 T  **9     ,T*i**(1-T**45*2)))(sum(
               [              Y(0,(A%3/3.+X%v+(X/v+
                               A/3/3.-x/2)/1j)*2.5
                             /x   -2.7,i)**2 for  \
                               A       in C
                                      [:9]])
                                        /9)
                                       )   )
-. .----------------------------------------------------
  Y
  ,,  ,---,
 (_,\/_\_/_\
   \.\_/_\_/>
   '-'   '-'
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list