We present FSHORNDROID, the first static analysis tool for Android applications, which is both flow-sensitive on the heap and provably sound with respect to a rich formal model of the Android platform. We formulate the analysis as a set of Horn clauses deifning a sound over-approximation of the semantics of the Android application to analyse, borrowing ideas from recency abstraction and extending them to a concurrent setting.

GitHub

Results

Publications

A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications Stefano Calzavara, Ilya Grishchenko, Adrien Koutsos, and Matteo Maffei In Proceedings of 30th Computer Security Foundations Symposium (IEEE CSF 2017). PDF Technical report

HornDroid: Practical and Sound Security Static Analysis of Android Applications by SMT Solving Stefano Calzavara, Ilya Grishchenko, and Matteo Maffei In Proceedings of 1st IEEE European Symposium on Security and Privacy (IEEE EuroS&P 2016). PDF Technical report

• HoRSt
  
• Wappler
  
• eThor
  
• EthSemantics
  
• TypeEQ
  

• back