goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
173 stars 72 forks source link

Taint analysis tutorial description #1090

Open sim642 opened 1 year ago

sim642 commented 1 year ago

It would be good if our taint analysis tutorial also had a nice documentation page like the signs tutorial has. It is currently very difficult to solve individually without a Goblint developer's instruction.

Right now it assumes familiarity with the taint analysis itself, which can be assumed from program analysis people who simply aren't Goblint developers, but cannot be assumed from students just getting into program analysis. Nor is there a reference to any description which explains what taint analysis wants to achieve and how it's supposed to do that.

The other issue is that simply looking at the taint.ml file, it's unclear in which order to implement the TODOs. For example, enter, return and combine_assign are only needed for the second interprocedural test, but one must already implement special, which comes after those in the source, to do anything for the first intraprocedural test.

michael-schwarz commented 1 year ago

I am skeptical of writing a tutorial on taint analyses for a larger audience, since we don't really do taint analysis. I think some sort of tutorial on how to use global invariants to accumulate some flow-insensitive information will be a lot more helpful, we regularly see students struggle with that.

sim642 commented 1 year ago

It's not for a larger audience. It's just so it's possible for a newcomer to Goblint to actually follow it. Right now it cannot be given to a student to solve without hand-holding.

michael-schwarz commented 1 year ago

For reference: GobTaint.pdf