<div dir="ltr">Dear Ahmet,<br><br><div class="gmail_quote"><div dir="ltr">ср, 7 нояб. 2018 г. в 8:04, A. Celenk <<a href="mailto:ahmet.celenk@procenne.com">ahmet.celenk@procenne.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<p>Hello Ilja,</p>
<p>Thanks a lot for great instructions! I'll be trying v2.0 in a
convenient time. By the way, reading through the steps, some
questions popped up in my mind:</p>
<p> - I assume we are downloading kernel 3.14.79 to verify it
(not to use it), so why do we build it? Isn't Klever performing
source code level analysis?<br></p></div></blockquote><div>There are two reasons for this. The first one is technical. Klever requires compilation commands to weave the source code of the program under verification to add generated environment models and assertions to check requirements (this is done aside from the provided source code). The second one is that Klever decomposes the program into fragments and generates environment models before verification, this step needs to extract a lot of information about the program (global variables, a callgraph). Clade collects all necessary information for Klever in this case.<br><br>Klever performs source code level analysis but it requires quite good environment models since it analyses not just separate independent functions but possible execution paths from entry points (main function, device driver initialization functions). For instance, for device drivers an environment model helps the software verification tool used in Klever as a backend to take into account that at initialization the driver registers callbacks and that these callbacks are called later with an appropriate order described in Klever environment model specifications.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div bgcolor="#FFFFFF" text="#000000"><p>
- Are we going to able to test our own drivers with this
release?<br><br></p></div></blockquote><div>Yes, this is possible. The simplest way is to place your drivers in kernel sources and compile them with the Clade as it can be done for any other Linux module or subsystem. If you prefer to compile them in a separate directory aside from the kernel source directory, then it is also possible but you need to add an extra path to "working source trees.json" (see the steps I described).<br>But note, that depending on the Linux kernel you are using you will need to adjust job.json in the web interface to choose the most suitable set of specifications. Also provided with the release specifications do not equally well support various Linux device drivers types.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div bgcolor="#FFFFFF" text="#000000"><p><br><br>
- Are we going to able to test just a simple e.g. "main.c"
file; or do we need a kernel?<br><br></p></div></blockquote><div>This is also possible, but Klever is intended for sound software verification to automatically prove program correctness relatively explicitly stated formalized requirements (this is not yet another bug finding tool). Used inside Klever software verification tools need to know about undefined functions (even for some functions from stdlib) and about how the program can interact with its environment (OS, other programs) to complete their proofs. In practice, this means that to obtain good results and get guarantees that your program is correct one need to provide models of some functions, describe program decomposition into fragments (if the program is larger than 100 thousands LoC) and do other steps that can be laborious sometimes.<br></div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div bgcolor="#FFFFFF" text="#000000"><p></p>
<p>Kind Regards,</p>
<p>Ahmet<br>
</p></div><div bgcolor="#FFFFFF" text="#000000">
<div class="m_901026549758533788moz-cite-prefix">On 6.11.2018 18:50, Ilja Zakharov
wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div>Dear Ahmet,</div>
<div><br>
As Evgeny Novikov promised (he is giving a talk at a
conference), below is the short guide for deploying and
running the Klever 2.0 software verification framework.<br>
</div>
<div><br>
</div>
<div>1. Choose your favorite Ubuntu/Debian image. The
instruction below is prepared for Ubuntu 18 but it not
strictly required.<br>
</div>
<div>2. Download and create a new desktop installation or
virtual machine with the system. Don't forget about our
hardware <a href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements" target="_blank">requirements</a>!<br>
</div>
<div>3. Download our software verification framework:</div>
<div>sudo apt-get install git<br>
</div>
<div>git clone <a href="https://github.com/ldv-klever/klever.git" target="_blank">https://github.com/ldv-klever/klever.git</a></div>
<div><br>
</div>
<div>4. Then follow <a href="https://klever.readthedocs.io/en/latest/deploy_local.html" target="_blank">deployment steps</a>
for the local deployment. In particular modify
klever-minimal.json.sample and save it as klever.json in
$KLEVER_SRC/deployment/conf/ directory. Also set environment
variables to specify $KLEVER_SRC directory with Klever source
files and target installation directory $KLEVER_DEPLOY_DIR.
Then install Klever with the command:<br>
sudo $KLEVER_SRC/deploys/bin/deploy-local
--deployment-directory $KLEVER_DEPLOY_DIR install production<br>
</div>
<div><br>
</div>
<div>5. After Klever installation you can build the kernel and
create build base. <br>
</div>
<div><br>
</div>
<div>Download the kernel: <br>
</div>
<div>
<div>wget <a href="https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz" target="_blank">https://cdn.kernel.org/pub/linux/kernel/v3.x/linux-3.14.79.tar.gz</a><br>
tar -xf linux-3.14.79.tar.gz<br>
<br>
</div>
<div>Install a suitable compiler:<br>
sudo update-alternatives --install /usr/bin/gcc gcc
/usr/bin/gcc-4.8 10<br>
sudo update-alternatives --config gcc</div>
<div>And choose 4.8 compiler there</div>
<div><br>
</div>
<div>Prepare your PATH environment variable:<br>
export PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH</div>
<div><br>
</div>
<div>Then run the following commands. It will take a lot of
time<br>
make allmodconfig<br>
clade-intercept make -j8 modules_prepare</div>
<div>clade-intercept -a make -j8 all</div>
<div>clade-all -p linux_kernel ./cmds.txt</div>
<div>echo "[\"$(readlink -f .)\"]" >
./clade/Storage/working source trees.json<br>
<br>
</div>
<div>6. Move this build base to another place. This is an
optional step but if you are going to build more bases in
this directory then it is better to do it. Note, then you
need a new base for each new configuration or kernel
version. <br>
</div>
<div>mv clade $NEW_PLACE/linux-3.14.79</div>
<div><br>
</div>
<div>7. Modify your deployment klever.json file in
$KLEVER_DEPLOY_DIR and add there a new section at the end of
the file in the root JSON object:<br>
"Klever Build Bases": ["$NEW_PLACE/linux-3.14.79"]</div>
<div><br>
</div>
<div>Instead of $NEW_PLACE set an absolute path to the
directory with your build base.<br>
<br>
</div>
<div>8 Update the Klever installation:<br>
sudo $KLEVER_SRC/deploys/bin/deploy-local
--deployment-directory $KLEVER_DEPLOY_DIR update production<br>
<br>
</div>
<div>9. Now you can run verification.<br>
</div>
<div>
<div>Open localhost:8998 in the web browser.</div>
<div>Input username: manager, password: manager.</div>
<div>Click "Linux 3.14".</div>
<div>Click Job->Edit or ->Copy and edit job.json and
other files depending on your needs.</div>
<div>In the job.json set "build base": "linux-3.14.79" or an
another name if you named your build base differently.<br>
</div>
<div>Before running any large target such as all modules
first try to verify modules given with the example.<br>
</div>
<div>10. Click Decision->Start.</div>
<div>11. Click "Start" or "Start with default values".</div>
<div>13. Wait for verification results. It can take very
much time especially if your hardware isn't powerful
enough. <br>
</div>
<div><br>
If you will meet some issues, please, report them to us.
We will try to solve or workaround them together. Note
also, that we renamed some files, so there are some
differences from the Klever-1.1 version in job files.<br>
<br>
</div>
<div>Best,<br>
</div>
<div>Ilia Zakharov</div>
</div>
</div>
<br>
<br>
<div class="gmail_quote">
<div dir="ltr">ср, 17 окт. 2018 г. в 10:40, Evgeny Novikov
<<a href="mailto:novikov@ispras.ru" target="_blank">novikov@ispras.ru</a>>:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>Dear Ahmet,</div>
<div> </div>
<div>Your primary question will not be resolved in Klever
2.0. So, I will answer it.</div>
<div> </div>
<div>In the deployment documentation you can find <a href="https://klever.readthedocs.io/en/latest/deploy.html#hardware-requirements" target="_blank">hardware
requirements</a>. I suggest that your VM does not meet
them, so, you either should empower it (I recommend this
to get better verification results faster) or use more
advanced settings. At page <a href="http://localhost:8998/service/schedulers/" target="_blank">http://localhost:8998/service/schedulers/</a>
you can find the maximum amount of computer resources that
Klever can spend for solving verification jobs and
verification tasks. In the file you attached there are
restrictions on computer resources just for verification
jobs. But verification tasks are solved during solving
verification jobs, so you should also take into account
maximum computer resources that are allowed for
verification tasks. Usually they are much more than ones
for verification jobs! These resources are specified
within file "tasks.json" at the job page, say, <a href="http://ldvdev:8998/jobs/5/" target="_blank">http://ldvdev:8998/jobs/5/</a>. I
hope that this is enough for you to proceed. </div>
<div> </div>
<div>For answering your second question it is definitely
necessary to wait for Klever 2.0 as it will be intended
for verification of C software rather than Klever 1.x that
can verify just Linux device drivers. But, please, do not
expect that Klever 2.0 will be able to verify some C
program without additional efforts. Our rich experience
and preliminary experiments show that one will need to
develop a suitable configuration and specifications for
each type of programs while verification tools like
CPAchecker do not handle unfamiliar code well sometimes.
If you are ready to invest much time, you are welcome! We
will be glad to hear some notes and remarks from you.</div>
<div> </div>
<div>-- </div>
<div href="http://mailto:novikov@ispras.ru">Evgeny Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org" target="_blank">http://linuxtesting.org</a></div>
<div> </div>
<div> </div>
<div> </div>
<div>17.10.2018, 09:12, "A. Celenk" <<a href="mailto:ahmet.celenk@procenne.com" target="_blank">ahmet.celenk@procenne.com</a>>:</div>
<blockquote type="cite">
<div bgcolor="#FFFFFF">
<p>Hello Evgeny,</p>
<p>Thank you very much for Klever, and for your help. I
will be eagerly waiting for 2.0 release. Till then, I
may try to use the current version to learn some
basics. Here is what I have done:</p>
<p>I could reach the web interface and managed to login
as manager, and played around a little bit. Considered
the warning on the deployment tutorial about messing
up the computer, I have installed Klever on a Ubuntu
18.04 VM. Being a VM, it has low resources. I have
started the preset Linux 3.14 job with default
configurations and got "Given resource limits for job
and tasks in sum are too high, we do not have such
amount of resources" error. Then I have checked out
manual configuration and used "paranoid development"
preset configuration, and lowered the resources as
much as I can (see my attached configuration).
Nevertheless I am still getting the same error and it
fails.</p>
<p>Here are my questions for the current release; if
answers would greatly change for v2.0, just ignore
these and I will be waiting for the new one:</p>
<p> - Is it fine to use Klever in such a
low-resourced VM? If so, what my configurations should
be? If not, what are the minimum system requirements
for Klever?<br>
- How do I upload a new job (e.g. just a single C
file, or a project with makefile)?</p>
<p>Thank you again,</p>
<p>Regards,</p>
<p>Ahmet</p>
<div>On <span>16-10-2018 18</span>:00, Evgeny Novikov
wrote:</div>
<blockquote type="cite">Also, I would like to inform you
that in a couple of weeks we will release Klever 2.0
that will change very many things related with core
functionalities. If you have time, then I recommend to
wait for this release and try it rather than a version
that will be deprecated soon.<br>
<br>
16:08, 16 октября 2018 г., Evgeny Novikov <a href="mailto:novikov@ispras.ru" target="_blank"><novikov@ispras.ru></a>:
<blockquote>
<div>
<div>16.10.2018, 13:55, "Evgeny Novikov" <<a href="mailto:novikov@ispras.ru" target="_blank">novikov@ispras.ru</a>>:</div>
<blockquote type="cite">
<div>Hello Ahmed,</div>
<div> </div>
<div>Your question is absolutely right. Klever
lacks user documentation and I think that it
will not have it in a near future. So, if you
would like to proceed, most likely you will
have many questions.</div>
<div> </div>
<div>You shouldn't run any script to start
Klever if deployment was successful. You just
need to open localhost:8998 in your web
browser.</div>
</blockquote>
<div><br>
I forgot to mention that there are 3 users
created in advance:</div>
<ul>
<li>The first one is Administrator (login:
admin, password: admin) that can change user
privileges. Most likely you will not need it
unlike you are going to create a multiuser
setup.</li>
<li>The second one is Manager (login: manager,
password: manager). This user can almost
everything and you should start with it!</li>
<li>The third one is Service user that serves
for internal purposes.</li>
</ul>
<div> </div>
<blockquote type="cite">
<div> </div>
<div>If you will have any other questions,
please, ask us. We will be glad to get some
feedback from you.</div>
<div> </div>
<div>-- </div>
<div href="http://mailto:novikov@ispras.ru">Evgeny
Novikov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org/" target="_blank">http://linuxtesting.org</a></div>
<div> </div>
<div> </div>
<div> </div>
<div>16.10.2018, 11:14, "A. Celenk" <<a href="mailto:ahmet.celenk@procenne.com" target="_blank">ahmet.celenk@procenne.com</a>>:</div>
<blockquote type="cite">
<p>Hello,<br>
<br>
I will ask a dumb question: How do we run
Klever? I've completed the<br>
deployment; but couldn't figure out which
python script (or some other<br>
thing) should I run to start testing.<br>
<br>
P.S: I've used example
klever-minimal.json.sample as configuration
file.<br>
<br>
Thanks a lot,<br>
<br>
Ahmet Celenk<br>
<br>
<br>
_______________________________________________<br>
ldv-project mailing list<br>
<a href="mailto:ldv-project@linuxtesting.org" target="_blank">ldv-project@linuxtesting.org</a><br>
<a href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project" target="_blank">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a></p>
</blockquote>
</blockquote>
</div>
</blockquote>
</blockquote>
</div>
</blockquote>
_______________________________________________<br>
ldv-project mailing list<br>
<a href="mailto:ldv-project@linuxtesting.org" target="_blank">ldv-project@linuxtesting.org</a><br>
<a rel="noreferrer" target="_blank" href="http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project">http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project</a><br><br></blockquote></div></div></blockquote></div></blockquote><div><br></div><div><div>-- </div>
<div href="http://mailto:novikov@ispras.ru">Ilia Zakharov<br>
Linux Verification Center, ISP RAS<br>
<a href="http://linuxtesting.org/" target="_blank">http://linuxtesting.org</a></div> </div></div></div>