Points-to analysis on Linux kernel about svf HOT 17 CLOSED

Hi Dae,

Have you tried "wpa -ander" instead of "wpa -nander"?

Both options produce the same points-to results. "-ander" is a fast fully optimized version of the standard transitive closure one "-nander".

Good luck!

from svf.

Thank you for your help!

Sadly, the amount of memory still causes the problem.
Are there parameters to reduce memory usage?
-mempar or others seem to be related to my problem.
I'm not an expert in static analysis, so I do not know what the parameters mean.

Otherwise, using more memory may be the only solution.

from svf.

How much memory have you used? My suggestion is to use at 64GB - 128GB machine for analyzing Linux kernels.

from svf.

I use 40gb (32+8 (the only spare I can use)).
The difference is not that big. I will buy more memory and try again.
Thank you!

from svf.

linux is not a toy. You need more memory to analyze it even using flow-insensitive andersen's analysis. Memory is also a bottleneck for analyzing large programs.

from svf.

Now I can do a points-to analysis with larger memory. So I close this issue.

from svf.

Would you mind sharing your results and the instructions for compiling and analyzing Linux?

Thanks

from svf.

Of course, I can.
But to be honest, what I said "I can" meant that I can just run the tool regardless of the accuracy of the result.
I got a bad result, in fact, almost useless.
If it is enough, I will share the instruction.

By the way, now I'm trying to get the "useful" result.
If you have any advice, please let me know.
Followings are my guessing of reasons that make the result bad.

First, I guess it is difficult for the tool to handle the kernel's global data properly.
(or, possibly, I did mistake when building the bitcode file and some global information is missing.)
I'm trying to figure it out with the additional function which calls all(or some) initcalls.
This function will be built and linked together with the kernel's bitcode file and I will try to analyze the whole bitcode file.
I expect that this function will be helpful in building the global information.

And it seems to lose points-to information when casting a pointer type variable to numeric-class type (e.g., unsigned long).

if (atomic_read(&files->count) == 1) {
...
    return (unsigned long)file;
  } else {
    ...
    return FDPUT_FPUT | (unsigned long)file;
}

In the above code, I think file(variable)'s points-to information is lost.

Lastly, I don't know why, but sometimes it seems to lose information when return.

static inline struct fd __to_fd(struct file* v)
{
  struct fd ret = (struct fd){(struct file *)(v) , 3};
  return ret;
}
static inline struct fd fdget(unsigned int fd)
{
  struct fd ret = __to_fd(__fdget(fd));
  return ret;
}

The above (slightly modified) kernel code, ret in __to_fd does points-to some memory object, but ret in fdget does points-to nothing.

Well, I'm not friendly with a static analysis and I may be wrong.
If I am wrong or you have any advice, please let me know.
I will continue to work on it, and I will let you know as soon as I get the good results.

from svf.

Have you tried to use gold-plugin instead of llvm-link to compile the code base? It will solve your incomplete code problem.

For a pointer to int casting, the integer is not a pointer type anymore, so it will point to nothing.
However, for an int to pointer casting, the pointer will point to a blackhole object when you enable "-blk" option.

from svf.

Thanks for the suggestion. Now I'm trying to build a linux kernel with llvm-gold plugin.
What I wonder is what is the difference between llvm-link and gold plugin? Do they link bitcode files differently?
What I did is link all of the generated bitcode with llvm-link, so I think an allocation site for global variables should be visible. Am I wrong?

from svf.

llvm-gold is to make sure the available bit code files are merged at linked time when emitting the executable.

You may also wish to refer to
http://llvm.org/docs/GoldPlugin.html

If you can make sure every c/c++ file is emitted to its bc file, then llvm-link should be the same as llvm-gold. However, in real-world applications, it is hard to use llvm-link because the file/folder hierarchies and makefile systems are complex.

from svf.

I open the other issue becuase my questions are too far from the original topic.

from svf.

Hi @threeearcat,
It has been almost two years but I wanted to ask about your experience analyzing the Linux bitcode with SVF. Can you give me rough numbers for the analysis time?

Thanks.

from svf.

@MuhammadAbuBakar95 I don't remember the kernel configuration I used, but the total amount of time was about or slightly shorter than a week for the entire kernel. I even don't remember my machine's spec. It surely depends on a kernel configuration so you may want to try SVF with the smallest kernel configuration.

from svf.

Thanks a lot for letting me know.

from svf.

@razzuser It may not be enough. My desktop has 64GB memory but it was not enough in my case so I used a server with 512GB memory.

And I kindly and politely ask you please not to mention another project here as I fully respect and appreciate SVF and its authors, so I am worrying that mentioning another project may be impolite.

from svf.

@threeearcat @razzuser No worries. I am happy with the discussions about analyzing Linux kernels. Please go ahead if you have any comments. Just in case someone else using SVF can benefit.

Thanks,

from svf.