{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T07:56:45Z","timestamp":1759564605165},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_21","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"296-311","source":"Crossref","is-referenced-by-count":15,"title":["Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System"],"prefix":"10.1007","author":[{"given":"Hendra","family":"Gunadi","sequence":"first","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. In: LICS, pp. 390\u2013401. IEEE Computer Society (1990)","DOI":"10.21236\/ADA323441"},{"key":"21_CR2","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: FSTTCS. LIPIcs, vol.\u00a02, pp. 49\u201360, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-29860-8_20","volume-title":"Runtime Verification","author":"D. Basin","year":"2012","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: Algorithms for monitoring real-time properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol.\u00a07186, pp. 260\u2013275. Springer, Heidelberg (2012)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-03466-4_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"A. Bauer","year":"2009","unstructured":"Bauer, A., Gor\u00e9, R., Tiu, A.: A first-order policy language for history-based transaction monitoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol.\u00a05684, pp. 96\u2013111. Springer, Heidelberg (2009)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-40787-1_4","volume-title":"Runtime Verification","author":"A. Bauer","year":"2013","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol.\u00a08174, pp. 59\u201375. Springer, Heidelberg (2013)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, pp. 721\u2013756. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"21_CR7","unstructured":"Brewer, D.F.C., Nash, M.J.: The Chinese wall security policy. In: IEEE Symposium on Security and Privacy. IEEE (1989)"},{"key":"21_CR8","unstructured":"Bugiel, S., Davi, L., Dmitrienko, A., Fischer, T., Sadeghi, A.-R., Shastry, B.: Towards taming privilege-escalation attacks on android. In: NDSS 2012 (2012)"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Chan, P.P.F., Hui, L.C.K., Yiu, S.-M.: Droidchecker: analyzing android applications for capability leak. In: WISEC, pp. 125\u2013136. ACM (2012)","DOI":"10.1145\/2185448.2185466"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-642-18178-8_30","volume-title":"Information Security","author":"L. Davi","year":"2011","unstructured":"Davi, L., Dmitrienko, A., Sadeghi, A.-R., Winandy, M.: Privilege escalation attacks on android. In: Burmester, M., Tsudik, G., Magliveras, S., Ili\u0107, I. (eds.) ISC 2010. LNCS, vol.\u00a06531, pp. 346\u2013360. Springer, Heidelberg (2011)"},{"issue":"7","key":"21_CR11","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"21_CR12","unstructured":"Dietz, M., Shekhar, S., Pisetsky, Y., Shu, A., Wallach, D.S.: Quire: Lightweight provenance for smartphone operating systems. In: 20th USENIX Security Symposium (2011)"},{"key":"21_CR13","unstructured":"Enck, W., Gillbert, P., Chun, B.-G., Cox, L.P., Jung, J., McDaniel, P., Sheth, A.N.: Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones. In: OSDI (2010)"},{"issue":"1","key":"21_CR14","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MSP.2009.26","volume":"7","author":"W. Enck","year":"2009","unstructured":"Enck, W., Ongtang, M., McDaniel, P.D.: Understanding android security. IEEE Security & Privacy\u00a07(1), 50\u201357 (2009)","journal-title":"IEEE Security & Privacy"},{"key":"21_CR15","unstructured":"Felt, A.P., Wang, H., Moschuk, A., Hanna, S., Chin, E.: Permission re-delegation: Attacks and defenses. In: 20th USENIX Security Symposium (2011)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer (1996)","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"21_CR17","unstructured":"Grace, M., Zhou, Y., Wang, Z., Jiang, X.: Systematic detection of capability leaks in stock android smartphones. In: NDSS 2012 (2012)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: A case study in the android operating system. CoRR, abs\/1311.2362 (2013)","DOI":"10.1007\/978-3-319-06410-9_21"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 196\u2013218. Springer, Heidelberg (1985)"},{"key":"21_CR21","unstructured":"Lineberry, A., Richardson, D.L., Wyatt, T.: These aren\u2019t the permissions you\u2019re looking for. In: DefCon 18 (2010)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-35632-2_13","volume-title":"Runtime Verification","author":"T. Reinbacher","year":"2013","unstructured":"Reinbacher, T., F\u00fcgger, M., Brauer, J.: Real-time runtime verification on chip. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol.\u00a07687, pp. 110\u2013125. Springer, Heidelberg (2013)"},{"key":"21_CR24","unstructured":"Schlegel, R., Zhang, K., Zhou, X., Intwala, M., Kapadia, A., Wang, X.: Soundcomber: A stealthy and context-aware sound trojan for smartphones. In: 18th Annual Network and Distributed System Security Symposium, NDSS (2011)"},{"key":"21_CR25","unstructured":"Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic specifications. In: Proc. of RV 2004 (2004)"},{"key":"21_CR26","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.entcs.2004.01.029","volume":"113","author":"P. Thati","year":"2005","unstructured":"Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic specifications. Electr. Notes Theor. Comput. Sci.\u00a0113, 145\u2013162 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T16:38:54Z","timestamp":1558888734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}