LogicDroid is a customized Android operating system which contains a custom reference monitor to check runtime violation of a given security policy. The security policy is specified in a logic-based language called recursive metric linear-time temporal logic (RMTL). The policy language can express complex security policies related to Android, including policies that check for privilege escalation attacks. The LogicDroid implementation includes modification of the Android middleware and its underlying Linux kernel to place various software sensors to detect events of interest, such as call chains among apps, or accesses to certain protected resources. The security policy itselfy can be modified on-the-fly on a running Android instance. The LogicDroid implementation includes an algorithm to generate a security monitor from a given policy specification in RMTL. Details of the algorithm can be found in the following research paper:
Hendra Gunadi and Alwen Tiu, Efficient runtime monitoring with metric temporal logic: a case study in the Android operating system. in FM 2014, ser. Lecture Notes in Computer Science, vol. 8442, 2014, pp. 296-311