199 citations · 260 across the 16 of their papers we have counts for
4 papers · 1 filter
A Type System for Privacy Properties (Technical Report)
Véronique Cortier, Niklas Grimm, Joseph Lallemand +1
Mature push button tools have emerged for checking trace properties (e.g. secrecy or authentication) of security protocols. The case of indistinguishability-based privacy propertie…
HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving
Stefano Calzavara, Ilya Grishchenko, Matteo Maffei
We present HornDroid, a new tool for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for sound…
A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications
Stefano Calzavara, Ilya Grishchenko, Adrien Koutsos +1
The present paper proposes the first static analysis for Android applications which is both flow-sensitive on the heap abstraction and provably sound with respect to a rich formal…
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet +7
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diver…