[ldv-project] Queries in running the LDV.

[Ilja Zakharov]

Hi Puneet,

Thanks for your interest in the Klever verification framework.

To verify your separate driver you should do the following steps:
1) First, be sure that you have some kernel version sources files to
compile your driver with. It is better to choose versions of Linux in
between 3.14 and 4.6.7. It is possible to check a driver with a newer
version of the Linux kernel but it will require additional steps. Both the
driver and Kernel should be configured and compiled for x86_64 architecture
preferably.

2) Install the Klever framework according to this manual:
https://klever.readthedocs.io/en/latest/deploy.html
(!) Klever will need a lot of computational resources to run, so avoid
installing it on a laptop. If your driver is an open source we can even
give you access to a virtual machine with Klever to try it.

3) Before trying to verify your own driver just ensure that all is
installed correctly. To do that open localhost:8998, log in as
manager:manager and try to solve a preexisting verification job there. If
all goes smoothly, go to the next step.

4) Prepare a build base for your driver. To do that just configure the
kernel and your driver and build it with a prefix command:

    clade-intercept <your compilation command>"

(An example: clade-intercept make -j8 M=drivers/net/usb)
Prepare the environment:
           export PATH=$KLEVER_DEPLOY_DIR/klever-addons/CIF/bin/:$PATH
Where $KLEVER_DEPLOY_DIR  is an absolute path to Klever installation
directory. Run "cif --help" to be sure that path is correct.
Then run the second command to create the build base:
           clade-all -p linux_kernel cmds.txt

After the command, you will have a directory named "clade". I refer to it
as <clade dir> in the next steps below.

5. After Klever installation, you can build the kernel and create a build
base.
a) Modify the configuration file that you have used for Klever installation
and add there the following entry: "Klever Build Bases": ["<clade dir>"]
b) Run again installation command exactly as at installation but replace
keyword "install" with "update"

6) That is almost all. Go to the web interface. Copy your test job, click
"modify", choose job.json file and in the opened editor window set proper
setting and identifiers of rules to check. You will need there to set
fields "build base" as "clade", "requirements" as ["linux:memory safety"]
(or add additional rules to check).

If you need an example write me back.

7) To uninstall Klever use installation command with command "uninstall"
instead of "install".

Please, do not hesitate to write me back and ask questions.

Best,
Ilia Zakharov

чт, 27 июн. 2019 г. в 20:57, Puneet Gupta <PUNEETG at xilinx.com>:

> Hi Alexey,
>
>
>
> Thanks for your mail.
>
>
>
> I have downloaded the klever package and managed to install it also by
> following the instructions given in the “local deployment” section.
>
> https://buildmedia.readthedocs.org/media/pdf/klever/latest/klever.pdf
>
>
>
> Can you guide me how to run the klever tool on my kernel module? Is there
> any doc which I can follow in which step by step the instructions are given?
>
>
>
> Currently I have my kernel module as a tar.bz2 and I want to do static
> analysis on it.
>
>
>
> I tried running ,
>
>    - cd bridge
>    - python3 manage.py test
>
>
>
> I got the following error:
>
> *  File "<frozen importlib._bootstrap>", line 219, in
> _call_with_frames_removed*
>
> *  File
> "/group/cdc_hd/members/puneetg/kernel_static_analysis/klever/klever-inst/klever/bridge/bridge/__init__.py",
> line 21, in <module>*
>
> *    from bridge.settings import DATABASES*
>
> *ModuleNotFoundError: No module named 'bridge.settings'*
>
>
>
> I can also see “linux-3.14.79.tar.xz” tar file in “build bases” directory.
> Shall I need to place my external module tar file in that directory and run
> some tests?
>
>
>
> Thanks,
>
> Puneet
>
>
>
>
>
> *From:* Alexey Khoroshilov <khoroshilov at ispras.ru>
> *Sent:* Friday, June 21, 2019 9:16 PM
> *To:* Puneet Gupta <PUNEETG at xilinx.com>; ldv-project at linuxtesting.org
> *Subject:* Re: Queries in running the LDV.
>
>
>
> EXTERNAL EMAIL
>
> Dear Puneet,
>
> It seems you use LDV Tools, but it was superseded by our newer KLEVER
> Framework [1,2].
> So, we suggest to use the newer tool.
>
> As for memory leak rule, we had a prototype of such rule in LDV Tools (104
> [3]), but it was not maintained and it is not available in KLEVER. So, we
> suggest to check code against some memory safety rules ((KLEVER rule id:
> "linux:memory safety", please note that string operations are not supported
> yet) or some Linux specific rules like mutex lock [4] or
> clock_enable/clock_disable [5].
>
> [1] http://linuxtesting.org/04-07-2018
> [2] https://forge.ispras.ru/projects/klever
> [3] https://forge.ispras.ru/issues/2735
> [4] https://forge.ispras.ru/issues/1940 (KLEVER rule ids:
> "linux:kernel:locking:mutex")
> [5] https://forge.ispras.ru/issues/8785 (KLEVER rule ids:
> "linux:drivers:clk1", "linux:drivers:clk2")
>
> Best regards,
> Alexey Khoroshilov
> Linux Verification Center, ISPRAS
>
>
> On 21.06.2019 8:30, Puneet Gupta wrote:
>
> Hi,
>
>
>
> I am using LDV for running static analysis for my external driver.
>
>
>
> I have few questions :
>
>    - The driver has many files to be compiled, but it seems the LDV is
>    only reporting out the errors for the file which is mentioned in ‘obj-m’.
>    How can I get result for all the files?
>    - What is meant by the error: “attempting to take field offset lock of
>    expression priv at stop whose value is Top”. I am getting only these
>    errors for my file.
>    - To test the LDV , I did kmalloc and didn’t freed the memory
>    returned. But the output on the webpage is not showing an error for that
>    memory leak. Have I need to pass some separate rule for detecting the
>    memory leaks?
>
>
>
> I am using 32_7a rule for running the driver, as given in the example in
> the LDV standard doc.
>
>
>
> Thanks,
>
> Puneet
>
> This email and any attachments are intended for the sole use of the named
> recipient(s) and contain(s) confidential information that may be
> proprietary, privileged or copyrighted under applicable law. If you are not
> the intended recipient, do not read, copy, or forward this email message or
> any attachments. Delete this email message and any attachments immediately.
>
>
> _______________________________________________
> ldv-project mailing list
> ldv-project at linuxtesting.org
> http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20190628/c97cda0f/attachment.html>