{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T13:21:19Z","timestamp":1730208079983,"version":"3.28.0"},"reference-count":37,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1109\/clei.2017.8226404","type":"proceedings-article","created":{"date-parts":[[2017,12,22]],"date-time":"2017-12-22T01:09:23Z","timestamp":1513904963000},"page":"1-10","source":"Crossref","is-referenced-by-count":5,"title":["Towards formal model-based analysis and testing of Android's security mechanisms"],"prefix":"10.1109","author":[{"given":"Gustavo","family":"Betarte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"Campo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maximiliano","family":"Cristia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felipe","family":"Gorostiaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camila","family":"Sanz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_5"},{"key":"ref32","volume":"9762","author":"dubois","year":"2016","journal-title":"Tests and proofs for enumerative combinatorics"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"ref30","first-page":"323","article-title":"A first step towards automated permission-enforcement analysis of the android framework","volume":"2","author":"arabnia","year":"2010","journal-title":"Proceedings of the 2010 International Conference on Security & Management SAM 2010"},{"volume":"9779","journal-title":"CAV 2016 ser Lecture Notes in Computer Science","year":"2016","key":"ref37"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1477"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0222-y"},{"key":"ref34","article-title":"Efficiently executable sets used by fireeye","author":"tuerk","year":"2016","journal-title":"The 8th Coq Workshop Nancy"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046779"},{"year":"2017","key":"ref11"},{"journal-title":"R styleable","year":"2017","key":"ref12"},{"journal-title":"Formal verification of the security model of Android Coq code","year":"2017","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2013.2284403"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1999995.2000018"},{"journal-title":"Practical Model-Based Testing A Tools Approach","year":"2006","author":"utting","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/32.553698"},{"journal-title":"The Z Notation A Reference Manual","year":"1989","author":"spivey","key":"ref18"},{"journal-title":"OVAL Language","year":"2017","key":"ref19"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.21236\/ADA579929"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.7561\/SACS.2016.1.27"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.29"},{"journal-title":"Deputy for Command and Management System USA Tech Rep","year":"1972","author":"anderson","key":"ref3"},{"journal-title":"The Coq Development Team The Coq Proof Assistant Reference Manual Version V8","year":"2016","key":"ref6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/SocialCom.2010.140"},{"journal-title":"Requesting permissions at run time","year":"2017","key":"ref5"},{"journal-title":"Platform Architect","year":"2017","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"journal-title":"Gartner Inc Tech Rep 2017","year":"2017","key":"ref2"},{"journal-title":"Application Fundamentals","year":"2017","key":"ref9"},{"journal-title":"Android Project","year":"2017","key":"ref1"},{"journal-title":"Ovaldi the OVAL Interpreter Reference Implementation","year":"2017","key":"ref20"},{"key":"ref22","article-title":"Increasing Android Security using a Lightweight OVAL-based Vulnerability Assessment Framework","author":"barr\u00e9re","year":"2012","journal-title":"Proceedings of IEEE SafeCon-fig '12"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/PST.2011.5971960"},{"key":"ref24","article-title":"Apex: extending android permission model and enforcement with user-defined runtime constraints","author":"nauman","year":"2011","journal-title":"Proc ASIACCS '10"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18178-8_29"},{"key":"ref26","article-title":"Permission re-delegation: Attacks and defenses","author":"felt","year":"2011","journal-title":"USENIX Security Symposium USENIX Association"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38592-6_20"}],"event":{"name":"2017 XLIII Latin American Computer Conference (CLEI)","start":{"date-parts":[[2017,9,4]]},"location":"Cordoba","end":{"date-parts":[[2017,9,8]]}},"container-title":["2017 XLIII Latin American Computer Conference (CLEI)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8171462\/8226362\/08226404.pdf?arnumber=8226404","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,1,29]],"date-time":"2018-01-29T22:15:34Z","timestamp":1517264134000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8226404\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":37,"URL":"https:\/\/doi.org\/10.1109\/clei.2017.8226404","relation":{},"subject":[],"published":{"date-parts":[[2017,9]]}}}