Alloy Model of Android Runtime Permission Model

This project presents a formal model of Android permissions for Android versions (6.0 and later) that use runtime permissions. We have also identified several flaws in this model and developed Cusper to systematically resolve these issues. Our paper, which won the distinguished paper award at The Network and Distributed System Security Symposium (NDSS) 2018, can be found here.