Our mobile devices, if compared to their desktop counterpart, store a lot of sensitive and private information. Considering how easily permissions to sensitive and critical resources in the mobile environment are released, for example in Android, sometimes the developer unwittingly causes the leakage of sensitive information, endangering the privacy of users. Starting from these considerations, in this paper we propose a method aimed to automatically localise the code where there is the possibility of information leak. In a nutshell, we discuss a method aimed to check whether a sensitive information is processed in a way that violates specific rules. We employ code instrumentation to annotate sensitive data exploiting model checking technique. To show the effectiveness of the proposed method a case study is presented.
Accidental sensitive data leaks prevention via formal verification
Ciobanu M. G.;Fasano F.;Mercaldo F.;Santone A.
2020-01-01
Abstract
Our mobile devices, if compared to their desktop counterpart, store a lot of sensitive and private information. Considering how easily permissions to sensitive and critical resources in the mobile environment are released, for example in Android, sometimes the developer unwittingly causes the leakage of sensitive information, endangering the privacy of users. Starting from these considerations, in this paper we propose a method aimed to automatically localise the code where there is the possibility of information leak. In a nutshell, we discuss a method aimed to check whether a sensitive information is processed in a way that violates specific rules. We employ code instrumentation to annotate sensitive data exploiting model checking technique. To show the effectiveness of the proposed method a case study is presented.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
