Mordente

This artifact contains Mordente, a tool for comparing different SEAndroid policies. Mordente is a model checker for the novel Comparative Modal Logic CML and implements the algorithms introduced in the corresponding paper "Differential Verification of Information Flow in SEAndroid Policies", by Lorenzo Ceragioli, Letterio Galletta, and Edoardo Lunati. Mordente takes as input a pair of SEAndroid policies and a file containing a list of CML formulas to verify. The artifact also includes an auxiliary tool to extract SEAndroid policies from Android images, so they can be passed as input to Mordente. As a minimal example, we provide a pair of simple policies and instructions for running a kick-the-tire test. Finally, we provide instructions to recover the real-world policies used in our paper for performance evaluation, and a script for replicating our results.