This week, we have the honor of hosting a presentation from Nassim Seghir, a Research Associate from University College London working for the DAASE project.
Nassim will give a talk about a really interesting topic, called TrueFlow, in which he is working at this moment. His aim is to improve static analysis, reducing false positives. He is extending FlowDroid with CBMC to measure the reachability of paths once FlowDroid declare them as data leaks.
Title:
Precise Analysis of Data Leaks
Abstract:
I’ll give an overview of the project TrueFlow, a master project that I have recently supervised. The purpose of TrueFlow is the reduction of false positives in static analysis tools. False positives are infeasible flows that a human assessor must consider and dismiss. First, we use FlowDroid, a state-of-the-art taint analysis tool, to find potential data leak paths. We then use CBMC, a C bounded model checker, to check the feasibility of those paths. I’ll report on two challenges we have tackled. First, we needed to reconstruct full paths as FlowDroid only provides some path projections. Second we needed to translate each path to the C language as it is the input for CBMC.