David Schneider

David Schneider

This is the former webpage of David Schneider.

GPG-Key: 4096R/7A058A55, Fingerprint: 1A49 4BF1 654E B122 F8EC 0ABE 42A9 5E9C 7A05 8A55.

My work is focused on the development of Cassandra, the Certifying App Store for Android. With Cassandra, a user can analyze applications for whether they reveal sensitive information that he wants to keep secret before installing them. Such information could be, e.g., his contacts, calendar entries, or current location. The meaning of security is precisely defined, based on a formal semantics of Android applications. The analysis implemented by Cassandra has been proven sound, meaning that it reliably detects all insecure applications. I am working on making Cassandra more widely applicable, more precise, and more efficient, while retaining its formal foundation and proven soundness.

Before joining the MAIS group, I obtained a Master’s and a Bachelor’s degree in computer science from Technische Universität Darmstadt, with a focus on mathematical logic during my Master’s studies. In both my theses I investigated a method to increase the precision of type-system-based information flow analyses of programs that use heap-allocated data structures.

Theses and Hiwi Positions

If you want to contribute to the development of Cassandra, either on the theoretical or on the practical side, please contact me via e-mail.

Research Interests

  • Formal methods
  • Formal semantics of programs
  • Static program analysis
  • Information flow security
  • Mathematical logic
  • Machine-assisted and automated theorem proving


These documents have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.







  • David Schneider. Instance-Specific Security Domain Assignments in Sequential Programming Languages. Bachelor Thesis, TU Darmstadt, 2012.
    BibTeX entry ]

Supervised Theses


  • Rune Fiedler. Towards Precise Treatment of Inter-Procedural Implicit Information Flow in Android Applications. Bachelor Thesis, TU Darmstadt, 2017
  • Thomas Höhl. Computing Security Certificates of Android Applications in Cassandra. Bachelor Thesis, TU Darmstadt, 2016


  • Thomas Höhl. Proving the Soundness of Cassandra's Security Type System in Isabelle/HOL. Studienarbeit

Services to the Scientific Community

I have reviewed papers for ESORICS 2017, LOPSTR 2016, GI Sicherheit 2016, and POST 2015.

Last modified on 30 January 2018.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang