<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta>
      <journal-title-group>
        <journal-title>Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves
Le Traon, Damien Octeau, and Patrick McDaniel. Flowdroid: Precise context, flow, field, object-sensitive
and lifecycle-aware taint analysis for android apps. ACM SIGPLAN Notices</journal-title>
      </journal-title-group>
    </journal-meta>
    <article-meta>
      <title-group>
        <article-title>Data Leakage in Java applets with Exception Mechanism</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Cinzia Bernardeschi</string-name>
          <email>cinzia.bernardeschi@unipi.it</email>
          <xref ref-type="aff" rid="aff2">2</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Paolo Masci</string-name>
          <email>paolo.masci@inesctec.pt</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Antonella Santone</string-name>
          <email>antonella.santone@unimol.it</email>
          <xref ref-type="aff" rid="aff1">1</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Department de Informatica, Universidade do Minho</institution>
          ,
          <addr-line>Braga</addr-line>
          ,
          <country country="PT">Portugal</country>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>Department of Bioscience and Territory, University of Molise</institution>
          ,
          <addr-line>Pesche (IS)</addr-line>
          ,
          <country country="IT">Italy</country>
        </aff>
        <aff id="aff2">
          <label>2</label>
          <institution>Department of Information Engineering, University of Pisa</institution>
          ,
          <country country="IT">Italy</country>
        </aff>
      </contrib-group>
      <pub-date>
        <year>2014</year>
      </pub-date>
      <volume>49</volume>
      <issue>6</issue>
      <fpage>259</fpage>
      <lpage>269</lpage>
      <abstract>
        <p>It is becoming more and more important to study methods for protecting sensitive data in computer and communication systems from unauthorized access, use, modification, destruction or deletion. Sensitive data include intellectual properties, payment information, personal files, personal credit card and other information depending on the business and the industry. Therefore, data leakage is considered an emerging security threat to organizations and companies. In this paper we present a static analysis method for information flow analysis in Java bytecode with exceptions. Exceptions are special events that break the normal execution flow. They can be used as a device to leak high security data since exception throwing can be accurately driven. The proposed analysis is capable of tracing information flow caused by exceptions by identifying instruction handler protected instructions as virtual control instructions. A malicious Java applet that clones the user secret PIN through exceptions is shown.</p>
      </abstract>
      <kwd-group>
        <kwd>Information Flow</kwd>
        <kwd>Data Leakage</kwd>
        <kwd>Java Exceptions</kwd>
      </kwd-group>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>
        Data leakage is defined as the accidental or unintentional distribution of private or sensitive data to
unauthorized entity [
        <xref ref-type="bibr" rid="ref14">17</xref>
        ]. Sensitive data include intellectual properties, payment information, personal
files, personal credit card and other information depending on the business and the industry. Facing the
challenges of data leakage requires complex and novel solutions.
      </p>
      <p>
        Java applets downloaded from the Internet are handled by the Java Security Manager that assigns
access privileges to their code and provides a customizable sandbox in which the Java bytecode runs.
Nevertheless, the access-control mechanism does not protect data confidentiality, since accessed data
could be unauthorizedly revealed by malicious applets to other applets that are not allowed to access
the data. On the other hand, the control of data propagation entails studying the flow of information in
the program [
        <xref ref-type="bibr" rid="ref4">7</xref>
        ]. For example, if data, besides having access rights, are also characterized by security
levels reflecting their privacy level, to check data leakage, we need to verify that data with high security
level are not transferred into lower security levels structures, since they could be read by low security
observers.
      </p>
      <p>This paper is an extension of the works [3], and checks data leakage in Java applets caused by
exceptions by using the same approach. Exceptions are special events that break the normal execution
flow. They can be used as a device to leak high security data since exception throwing can be accurately
driven. The method is based on information flow analysis and abstract interpretation of the bytecode.
Information flow analysis is considered one of the main techniques for studying security in computer
systems. In particular, information flow properties are a particular class of security properties which
aim at controlling the way information may flow among different entities. Assuming the security
constraints to be known, the approach maps data confidentiality within a multi-level security model, where
private data are mapped to high security level and public data are mapped to low security level.
Programs are then executed on security levels instead of real data. Programs are analyzed on a per-method
basis with an iterative data-flow approach, and reaches a fix-point when a structure, called the security
context, agrees for all methods. The security context contains information about the security levels by
which each method has been verified and it is at the basis of the assume-guarantee principle used by the
static analysis. The analysis is capable of tracing information flow caused by exceptions by identifying
instruction handler protected instructions as virtual control instructions. Since the bytecode is
unstructured, the region of influence of each protected instruction is computed by analysing the control flow
graph of each method. A malicious Java applet that clones the user secret PIN through the exception
mechanism has been considered as a proof of concept of our methodology. Although our study is a
preliminary work, the results seem promising and a performance evaluation, larger discussions and greater
experimentations are still in progress.</p>
      <p>
        Several approaches have been developed for data leakage using information flow analysis. In [
        <xref ref-type="bibr" rid="ref5">8</xref>
        ] a
dynamic mechanism for securing script executions by tracking information flow in JavaScript and its
APIs is presented. In [
        <xref ref-type="bibr" rid="ref7">10</xref>
        ] JOANA is presented, which comes as an add-on for the Eclipse IDE. It is
object, flow and context-sensitive as well and is used for analyzing Java bytecode for noninterference
and information flow control. It can also detect leaks that result from the interleaving of different
threads. However, JOANA requires annotations to be present in the code during development. In [
        <xref ref-type="bibr" rid="ref8">11</xref>
        ]
the authors use Program Dependence Graphs (PDGs) for representing the flows of information found in
Java bytecode and use a custom PDG query language to allow users to express their own
applicationspecific security policies, without interfering with the development of the program. Many applications
of information flow analysis have been proposed also for Android Applications. SCanDal [
        <xref ref-type="bibr" rid="ref10">13</xref>
        ], a sound
and automatic static analyzer, exploits abstract interpretation to detect privacy leaks in Android apps.
IccTA [
        <xref ref-type="bibr" rid="ref11">14</xref>
        ] uses a static taint analysis technique to find privacy leaks, i.e., paths from sensitive data,
called sources, to statements sending the data outside the application or device, called sinks. A path may
be within a single component or cross multiple components. IccTA relies on Epicc [
        <xref ref-type="bibr" rid="ref13">16</xref>
        ] and FlowDroid
[1] to find data leaks between components of Android applications. They can both detect intra- and
inter-component leaks within a single application or between multiple applications.
      </p>
      <p>
        Our approach is based on abstract interpretation of the operational semantics, therefore the analysis
can be fully automated. Moreover, the approach is modular, and it has been applied for checking
leakages between packages in Java cards real applications [2], and to analyse data secure flow in Autosar
security annotated models for automotive applications [
        <xref ref-type="bibr" rid="ref3">6</xref>
        ].
2
      </p>
    </sec>
    <sec id="sec-2">
      <title>Exception handling in the Java language</title>
      <p>Exceptions are special events used for signaling errors during the execution of a program. The rising
of an exception is referred as throwing. Every time an exception is thrown, the Java runtime system
breaks the standard execution flow of the program and calls the handler that catches and manages the
exception. The correct handler for a given exception type can be found searching backwards through
the call stack of the method: if no appropriate handler is found the program terminates.</p>
      <p>
        Exceptions can be explicitly thrown by a program with the throw statement or they can automatically
be thrown by the Java Virtual Machine whenever it detects an abnormal execution condition of a program
(i.e., a Java programming language constraint violation) [
        <xref ref-type="bibr" rid="ref6">9</xref>
        ]. The exception type is specified by passing
an object to the Java runtime system: it is an instance of the throwable class and it contains information
about the program state and the kind of error occurred.
      </p>
      <p>In the high level Java programming language exceptions are described with try-catch blocks: try
blocks contain protected instructions, i.e., instructions whose exceptions are handled by the method,
while catch blocks contain the body of implemented handlers. Instructions can be protected by more
Object
Throwable</p>
      <p>Exception
Error</p>
      <p>Runtime
...</p>
      <p>I/O
Class Not Found
Virtual Machine Error
...</p>
      <p>Linkage
AWT</p>
      <p>Index Out Of Bounds</p>
      <p>Null Pointer</p>
      <p>...</p>
      <p>Class Cast
Out Of Memory
Stack Overflow
...</p>
      <p>Unknown
than one handler since any try block can be followed by many catch blocks, one for each possible thrown
exception.</p>
      <p>From a low-level point of view the bytecode contains the body of implemented handlers and an
exception table which contains their descriptors. For each handler, the descriptors specify the type of
the handled exception and the fragment of protected code. The handlers code is usually not directly
targeted by any instruction of the method: the standard Java compiler follows this behavior.
2.1</p>
      <p>Exception Types
In the Java platform the Throwable class is the superclass of all errors and exceptions (see Figure 1).</p>
      <p>Java exceptions can be grouped into two categories: checked and unchecked. Checked exceptions
represent error conditions that can be foreseen by the programmers. Code fragments containing this
kind of exceptions must declare them and must have an appropriate handler: the Java compiler enforces
these constraints. On the other hand, the unchecked exceptions are linked to conditions that should
never happen during the execution of well-written programs (i.e., the access of array elements out of the
array bounds) or to severe Virtual Machine errors (i.e., out of memory or stack overflow). They can be
handled by exception handlers although it is not required and there is no compile-time checking. The
Java programming language allows programmers to declare user-defined exceptions, of both checked
and unchecked type.
3</p>
    </sec>
    <sec id="sec-3">
      <title>The method</title>
      <p>Data leakage is directly connected to the violation of the secure information flow in programs. Given a
program P, in which each variable is assigned a security level, P has a secure information flow if, when
P terminates, the value of each variable with low security level does not depend on the initial value of
variables with high level. Let us suppose that variable x has a security level higher than the one assigned
to variable y: examples of violation of secure information flow in high level languages are (i) y=x and
(ii) if (x==0) fy=1;g else fy=0;g. In the first case there is an explicit information flow from x
to y, while in the second case there is an implicit information flow. In both cases the final value of y
reveals information on the value of the higher security variable x.</p>
      <p>The proposed method checks for the secure information flow property in the Java platform by
statically analysing the applet bytecode before its real execution within a multi-level security model. The
security model assigns to any applet input/ouput channel a security level. The files containing private
information will be characterized by high security levels, while the public files will be characterized
by low security levels. We split files into two disjoint sets of high and low security files. The secure
information flow property determines whether highly secure (private) data are kept secret.
Definition 1. Given a security policy and a terminating application, the application satisfies the secure
information flow property if the contents of every low security output file do not depend on the contents
of the high security input files.</p>
      <p>
        This property is also called non-interference in the literature. The analysis is based on the abstract
interpretation approach proposed in [3], that has been proved to capture all the illegal flows of data. A
notion of non-interference for real-time systems specified by timed automata has been also introduced
in [
        <xref ref-type="bibr" rid="ref1">4</xref>
        ].
      </p>
      <p>
        We trace data propagation in a Java applet by checking its methods, one by one, with a bytecode
data-flow analysis on the domain of security levels. The information flow inside a method is propagated
by inferring the security level of each Virtual Machine register (stack locations and local variables).
The analysis directly catches the explicit information flow by observing the security level of instruction
operands during the abstract execution of the code. The implicit information flow, instead, is propagated
and caught by computing control regions [
        <xref ref-type="bibr" rid="ref9">12</xref>
        ]: each bytecode instruction is being verified under a
security environment that takes into account the security level of all the control conditions an instruction
is affected by. Data propagation caused by any method invocation and the access to common data
structures in the heap is studied by executing each method inside a security context; the security context
sets the security levels of object fields in the heap and the security level of input/output and return
parameters of each method. The secure information flow analysis corresponds to an iterative verification
of all methods within a common security context: it stops when a fix-point is reached.
      </p>
      <p>Example of secure information flow violation are shown below. The bytecode fragment in the
Listing 1 shows an explicit flow from x to y. In the bytecode, x is the register 1, while y is the register 2,
respectively.
1 . . . . . . . . .
2 4 : i l o a d 1
3 5 : i s t o r e 2
4
5 . . . . . . .</p>
      <p>/ / l o a d x on t h e s t a c k
/ / s t o r e t h e t o p o f
/ / t h e s t a c k o n t o y
Listing 1: Explicit flow
1 . . . . .
2 6 : i l o a d 1
3 7 : i f n e 15
4 1 0 : i c o n s t 1
5 1 1 : i s t o r e 2
6
7 1 2 : g o t o 17
8 1 5 : i c o n s t 0
9 1 6 : i s t o r e 2
10
11 . . . . .</p>
      <p>/ / l o a d x on t h e s t a c k
/ / jump i f n o t e q u a l
/ / l o a d 1 on t h e s t a c k
/ / s t o r e t h e t o p o f
/ / t h e s t a c k o n t o y
/ / l o a d 0 on t h e s t a c k
/ / s t o r e t h e t o p o f
/ / t h e s t a c k o n t o y</p>
      <sec id="sec-3-1">
        <title>Listing 2: Implicit flow</title>
        <p>The bytecode in Listing 2 shows an implicit flow from x to y. The final value of y is equal to 0 or 1
depending on the value of x.</p>
        <p>We use the control flow graph and the notion of control region for modeling implicit information
flows. Given a control instruction i, the control region of i is the set of instructions that can be executed
conditionally according to i. For example, the control region of an if is the set of instructions in the
two branches of the if, until the point at which the two branches join. In the analysis, the level of the
implicit flow affecting an instruction is represented by the security environment.</p>
        <p>Let us consider the control flow graph of the bytecode in Listing 2, shown in Figure 2 (b). Since
the condition of the if at address 7 is H (x is a high variable), and the control region of 7 is
f10; 11; 12; 15; 16g, both iconst instructions are executed in a high security environment. Therefore
 iload_1   4 
istore_2   5 
a high value is pushed on the stack, and the high value is stored into the low security variable y.</p>
        <p>An example of security context is the following, where A is a class with data member f1 and method
member mt1; B a class with data member f2 and method member mt2 and mt3. In particular, for each
method, the security context maintains the level of parameters, return and the security environment.
SECURITY CONTEXT
classfields, arrays
A.f1 = L
methods of class A
mt1(L, H)L; L</p>
        <p>B.f2 = H
methods of class B
mt2(L)L; L
mt3(L)L; L</p>
      </sec>
    </sec>
    <sec id="sec-4">
      <title>4 Information leakage with the exception mechanism</title>
      <p>The Java code of a simple example with exceptions is shown in Listing 3 and the corresponding Java
bytecode is shown in Listing 4.
1
2 i m p o r t j a v a . i o . I O E x c e p t i o n ;
3 p u b l i c c l a s s H e l l o f
4 p u b l i c s t a t i c v o i d main ( S t r i n g [ ] a r g s ) f
5 g
6
7 p u b l i c v o i d stampa ( S t r i n g s ) f
8 System . o u t . p r i n t l n ( ” O u t s i d e ” ) ;
9
10
11
12
13 System . o u t . p r i n t l n ( ” P r i n t . . . ” ) ;
14 g
15 g
t r y f System . o u t . p r i n t l n ( ” I n s i d e t r y ” ) ; g
c a t c h ( A r i t h m e t i c E x c e p t i o n e ) f System . o u t . p r i n t l n ( ” P r i n t c a t c h ” ) ; g</p>
      <sec id="sec-4-1">
        <title>Listing 3: Simple Java Example</title>
        <p>p u b l i c v o i d s t a m p a ( j a v a . l a n g . S t r i n g ) ;</p>
        <p>Code :
0 : g e t s t a t i c #2 / / F i e l d j a v a / l a n g / System . o u t : L j a v a / i o / P r i n t S t r e a m ;
3 : l d c #3 / / S t r i n g O u t s i d e
5 : i n v o k e v i r t u a l #4 / / Method j a v a / i o / P r i n t S t r e a m . p r i n t l n : ( L j a v a / l a n g / S t r i n g ; ) V
8 : g e t s t a t i c #2 / / F i e l d j a v a / l a n g / System . o u t : L j a v a / i o / P r i n t S t r e a m ;
1 1 : l d c #5 / / S t r i n g I n s i d e t r y
1 3 : i n v o k e v i r t u a l #4 / / Method j a v a / i o / P r i n t S t r e a m . p r i n t l n : ( L j a v a / l a n g / S t r i n g ; ) V
1 6 : g o t o 28
1 9 : a s t o r e 2
2 0 : g e t s t a t i c #2 / / F i e l d j a v a / l a n g / System . o u t : L j a v a / i o / P r i n t S t r e a m ;
2 3 : l d c #7 / / S t r i n g P r i n t c a t c h
2 5 : i n v o k e v i r t u a l #4 / / Method j a v a / i o / P r i n t S t r e a m . p r i n t l n : ( L j a v a / l a n g / S t r i n g ; ) V
2 8 : g e t s t a t i c #2 / / F i e l d j a v a / l a n g / System . o u t : L j a v a / i o / P r i n t S t r e a m ;
3 1 : l d c #8 / / S t r i n g P r i n t . . .
3 3 : i n v o k e v i r t u a l #4 / / Method j a v a / i o / P r i n t S t r e a m . p r i n t l n : ( L j a v a / l a n g / S t r i n g ; ) V
3 6 : r e t u r n</p>
      </sec>
      <sec id="sec-4-2">
        <title>Listing 4: Simple Java Bytdecode Example</title>
        <p>From the exception table, as shown in the bottom of Listing 4, we derive that instructions from 8
to 16 are executed in a protected way. Moreover, 19 is the first instruction of the exception handler.
Instruction 8 is protected and it may throw an exception, that can be captured by an exception handler
(executing the code at 19).</p>
        <p>Assume that a protected instruction is a control instruction that throws an exception depending on
an high condition. The handler of the exception must be executed under a security environment that is
high. The execution of the exception handler that captures the exception may reveal information on the
value of the high condition, thus causing a leakage of information.</p>
        <p>From this point of view, the handlers body can be thought as particular extensions of the methods
code. An extended control flow graph can be defined as the graph obtained from the method graph
augmented with edges starting from protected instructions to the first instruction of the protecting handlers.</p>
        <p>Figure 3 shows the extended control flow graph of the bytecode shown in Listing 4.
1 i m p o r t j a v a . i o . I O E x c e p t i o n ;
2
3 p u b l i c c l a s s P i n C l o n e r f
4 p u b l i c s t a t i c v o i d main ( S t r i n g [ ] a r g s ) f
5 g
6
7 p u b l i c v o i d P i n C l o n e r ( ) f
8 t r y f
9 i n t p ;
10
11
12
13
14
15
16
17
18
19
20
21
22 g
f o r ( . . . ) f / / r e a d s a c h a r from PIN FILE and s t o r e i t i n p ;
. . . . .
i f ( p == 0 ) f t h r o w new A r i t h m e t i c E x c e p t i o n ( ) ; g
e l s e f t h r o w new N u l l P o i n t e r E x c e p t i o n ( ) ; g
g</p>
        <p>Under this point of view, the bytecode instructions act like virtual control instructions if they are
contained in a section protected by handlers. This is due to the protected instructions run-time behavior:
they can jump to their standard successors or to the starting of their exception handlers.</p>
        <p>Notice that the exception handlers of a method can be exhaustively identified by inspecting the
handler descriptor table of the method; moreover their code must be abstractly executed after all protected
instructions since any execution flow has to be considered.</p>
        <p>The region of influence of the protected instructions is computed on the extended control flow graph,
highlighted by a box in Figure 3. Since the throw instruction in a method is similar to a return statement,
the exceptions can be used as a vehicle to deliver information (on occurred errors) between methods. As
well as for the return value of methods, the security context must contain identifiers for all the possible
thrown exceptions of each method.</p>
        <p>getsta/c   0 
ldc  </p>
        <p>3 
5</p>
      </sec>
    </sec>
    <sec id="sec-5">
      <title>The PINCloner malicious applet</title>
      <p>Let us consider the PINcloner applet, where Pin file and Clone file are the input and the output
files, respectively. Pin file is a private file containing a secret PIN (a sequence of 0/1 characters, for
simplicity). Let us suppose that the PINcloner application can read from the private file. The applet
clones the user secret PIN with the exception mechanism. After every character has read, it will be
written in a the public file by the handler of the exception.</p>
      <p>In particular, the PINCloner application clones the characters of the Pin file by throwing different
kind of exceptions depending on the value read (NullPointerException and ArithmeticException). The
exceptions are thrown directly with a throw statement. A fragment of the source code is shown in Listing
5 and the bytecode in Listing 6.</p>
      <p>The Exception table, at the bottom of Listing 6, shows that the instructions from 0 to 22 are protected
by two exception handles starting at instruction 22 and instruction 34, respectively.</p>
      <p>Instruction 3 is an if with four successors: the natural successors, plus the two entry points of the
exception handlers. The control region of 3 includes the instructions of the exception handlers, and
consequently these instructions are executed in a security environment given by the condition of the
ifne. Since the condition depends on the 0/1 value of PIN character read from a high security file, the
iconst_1   0 
istore_1   1 
implicit flow is high. The handler of the exception, write such value into the low security Clone file
file. The application violates the secure information flow because high security data are written on a
public file and our methodology successfully detects this data leakage.
6</p>
    </sec>
    <sec id="sec-6">
      <title>Conclusion and Future Work</title>
      <p>
        In this paper a static information flow based method for data leakage detection has been presented. The
method applies to Java bytecode with exceptions. Exception are special events that break the normal
execution flow. They can be used as a device to leak high security data since exception throwing can be
accurately driven. The proposed analysis is capable of tracing information flow caused by exceptions by
identifying instruction handler protected instructions as virtual control instructions. A malicious Java
program that clones the user secret PIN through exception has been analysed, with encouraging results.
The approach scales up because methods are analysed one at a time until the fixpoint is reached. The
main drawback of the approach is that not all secure programs are accepted because of the approximation
of the abstract interpretation approach. For example, when the same method is invoked at different
points, it is verified under the highest security level for parameters and returns. This causes the detection
of false illegal flows. As future work, we plan to extend our methodology for Android applications. The
idea is to extract the class files of an Android application, using, for example, dex2jar1 tool in order to
convert the dex (i.e., the Dalvik Executable) file into jar (i.e., Java Archive) file. Using the dex2jar tool,
we obtain the Android application in a compressed format. To extract the classes from the jar file, we
can use the command: jar -xvf provided by the Java Development Kit. The outputs of this package
are the classes relative to the the Android application and our methodology is directly applicable [
        <xref ref-type="bibr" rid="ref12 ref2">15, 5</xref>
        ].
      </p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          [4]
          <string-name>
            <given-names>Roberto</given-names>
            <surname>Barbuti</surname>
          </string-name>
          , Nicoletta De Francesco, Antonella Santone, and
          <string-name>
            <given-names>Luca</given-names>
            <surname>Tesei</surname>
          </string-name>
          .
          <article-title>A notion of non-interference for timed automata</article-title>
          .
          <source>Fundam</source>
          . Inform.,
          <volume>51</volume>
          (
          <issue>1-2</issue>
          ):
          <fpage>1</fpage>
          -
          <lpage>11</lpage>
          ,
          <year>2002</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          [5]
          <string-name>
            <given-names>Pasquale</given-names>
            <surname>Battista</surname>
          </string-name>
          , Francesco Mercaldo, Vittoria Nardone, Antonella Santone, and Corrado Aaron Visaggio.
          <article-title>Identification of android malware families with model checking</article-title>
          .
          <source>In Proceedings of the 2nd International Conference on Information Systems Security and Privacy</source>
          ,
          <string-name>
            <surname>ICISSP</surname>
          </string-name>
          <year>2016</year>
          , Rome, Italy,
          <source>February 19-21</source>
          ,
          <year>2016</year>
          ., pages
          <fpage>542</fpage>
          -
          <lpage>547</lpage>
          . SciTePress,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          [6]
          <string-name>
            <given-names>Cinzia</given-names>
            <surname>Bernardeschi</surname>
          </string-name>
          , Marco Di Natale, Gianluca Dini, and
          <string-name>
            <given-names>Maurizio</given-names>
            <surname>Palmieri</surname>
          </string-name>
          .
          <article-title>Verifying data secure flow in autosar models by static analysis</article-title>
          .
          <source>In 1st International Workshop on FORmal methods for Security Engineering</source>
          , pages
          <fpage>704</fpage>
          -
          <lpage>713</lpage>
          ,
          <year>2017</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          [7]
          <string-name>
            <given-names>P. J.</given-names>
            <surname>Denning</surname>
          </string-name>
          . D. E. Denning.
          <article-title>Certification of programs for secure information flow</article-title>
          .
          <source>Communications of the ACM</source>
          ,
          <volume>20</volume>
          (
          <issue>7</issue>
          ):
          <fpage>504</fpage>
          -
          <lpage>513</lpage>
          ,
          <year>1977</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          [8]
          <string-name>
            <given-names>Andrew</given-names>
            <surname>Ferraiuolo</surname>
          </string-name>
          , Weizhe Hua, Andrew C Myers, and
          <string-name>
            <given-names>G Edward</given-names>
            <surname>Suh</surname>
          </string-name>
          .
          <article-title>Secure information flow verification with mutable dependent types</article-title>
          .
          <source>In Proceedings of the 54th Annual Design Automation Conference</source>
          <year>2017</year>
          ,
          <article-title>page 6</article-title>
          . ACM,
          <year>2017</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          [9]
          <string-name>
            <given-names>J</given-names>
            <surname>Gosling</surname>
          </string-name>
          ,
          <string-name>
            <given-names>B</given-names>
            <surname>Joy</surname>
          </string-name>
          , G. Steele, and
          <string-name>
            <given-names>G.</given-names>
            <surname>Bracha. The Java Language Specification</surname>
          </string-name>
          , Second Edition. AddisonWesley Publishing Company, Reading, Massachusetts,
          <year>2000</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          [10]
          <string-name>
            <given-names>Christian</given-names>
            <surname>Hammer</surname>
          </string-name>
          and
          <string-name>
            <given-names>Gregor</given-names>
            <surname>Snelting</surname>
          </string-name>
          .
          <article-title>Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs</article-title>
          .
          <source>Int. J. Inf. Sec.</source>
          ,
          <volume>8</volume>
          (
          <issue>6</issue>
          ):
          <fpage>399</fpage>
          -
          <lpage>422</lpage>
          ,
          <year>2009</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          [11]
          <string-name>
            <given-names>Andrew</given-names>
            <surname>Johnson</surname>
          </string-name>
          , Lucas Waye,
          <string-name>
            <given-names>Scott</given-names>
            <surname>Moore</surname>
          </string-name>
          , and
          <string-name>
            <given-names>Stephen</given-names>
            <surname>Chong</surname>
          </string-name>
          .
          <article-title>Exploring and enforcing security guarantees via program dependence graphs</article-title>
          .
          <source>In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation</source>
          , Portland,
          <string-name>
            <surname>OR</surname>
          </string-name>
          , USA, June 15-17,
          <year>2015</year>
          , pages
          <fpage>291</fpage>
          -
          <lpage>302</lpage>
          . ACM,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          [12]
          <string-name>
            <given-names>R.</given-names>
            <surname>Johnson</surname>
          </string-name>
          ,
          <string-name>
            <given-names>D.</given-names>
            <surname>Pearson</surname>
          </string-name>
          , and
          <string-name>
            <given-names>K.</given-names>
            <surname>Pingali</surname>
          </string-name>
          .
          <article-title>The program structure tree: Computing control regions in linear time</article-title>
          .
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          [13]
          <string-name>
            <surname>Jinyung</surname>
            <given-names>Kim</given-names>
          </string-name>
          , Yongho Yoon, Kwangkeun Yi, and Junbum Shin.
          <article-title>ScanDal: Static analyzer for detecting privacy leaks in android applications</article-title>
          . In Hao Chen, Larry Koved, and Dan S. Wallach, editors,
          <source>MoST 2012: Mobile Security Technologies</source>
          <year>2012</year>
          , Los Alamitos, CA, USA, May
          <year>2012</year>
          . IEEE.
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          [14]
          <string-name>
            <surname>Li</surname>
            <given-names>Li</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>Alexandre</given-names>
            <surname>Bartel</surname>
          </string-name>
          , Tegawende´ F Bissyande´,
          <string-name>
            <surname>Jacques</surname>
            <given-names>Klein</given-names>
          </string-name>
          , Yves Le Traon, Steven Arzt, Siegfried Rasthofer, Eric Bodden, Damien Octeau, and
          <string-name>
            <surname>Patrick McDaniel</surname>
          </string-name>
          .
          <article-title>Iccta: Detecting inter-component privacy leaks in android apps</article-title>
          .
          <source>In Proceedings of the 37th International Conference on Software Engineering-Volume</source>
          <volume>1</volume>
          , pages
          <fpage>280</fpage>
          -
          <lpage>291</lpage>
          . IEEE Press,
          <year>2015</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          [15]
          <string-name>
            <surname>Francesco</surname>
            <given-names>Mercaldo</given-names>
          </string-name>
          , Vittoria Nardone, Antonella Santone, and Corrado Aaron Visaggio.
          <article-title>Download malware? no, thanks: how formal methods can block update attacks</article-title>
          .
          <source>In Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE</source>
          <year>2016</year>
          , Austin, Texas, USA, May
          <volume>15</volume>
          ,
          <year>2016</year>
          , pages
          <fpage>22</fpage>
          -
          <lpage>28</lpage>
          . ACM,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          [16]
          <string-name>
            <surname>Damien</surname>
            <given-names>Octeau</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Patrick</surname>
            <given-names>McDaniel</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>Somesh</given-names>
            <surname>Jha</surname>
          </string-name>
          , Alexandre Bartel, Eric Bodden, Jacques Klein, and Yves Le Traon.
          <article-title>Effective inter-component communication mapping in android: An essential step towards holistic security analysis</article-title>
          .
          <source>In Presented as part of the 22nd USENIX Security Symposium (USENIX Security 13)</source>
          , pages
          <fpage>543</fpage>
          -
          <lpage>558</lpage>
          ,
          <year>2013</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          [17]
          <string-name>
            <surname>Asaf</surname>
            <given-names>Shabtai</given-names>
          </string-name>
          , Yuval Elovici, and
          <string-name>
            <given-names>Lior</given-names>
            <surname>Rokach</surname>
          </string-name>
          .
          <article-title>A Survey of Data Leakage Detection</article-title>
          and
          <string-name>
            <given-names>Prevention</given-names>
            <surname>Solutions</surname>
          </string-name>
          . Springer Publishing Company, Incorporated,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>