-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathtools.html
More file actions
145 lines (122 loc) · 6.24 KB
/
tools.html
File metadata and controls
145 lines (122 loc) · 6.24 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
<title>Damien Octeau</title>
<link href="css.css" rel="stylesheet" type="text/css">
<script src="js/ga.js"></script>
</head>
<body>
<table cellspacing="0" cellpadding="5px">
<tr> <td class="myname">Damien Octeau</td> </tr>
<tr> <td id="nav" class="mylinks"> <myl> <a href="index.html" class="linknostyle">Home</a> ◊ <a href="research.html" class="linknostyle">Research</a> ◊ <a href="publications.html" class="linknostyle">Publications</a> ◊ <a href="vita.html" class="linknostyle">Vita</a> ◊ <strong>Tools</strong> </myl> </td> </tr>
</table>
<div class="content">
<h3>PRIMO</h3>
<p>Despite the many techniques devised to increase the precision of
static analysis results, the results precision is often not high
enough for large scale analysis. This is because the static inference
of many properties is undecidable, and others are too computationally
expensive. This is especially problematic with the rise of centralized
application markets, where market providers may want to verify
properties (e.g., security) in their entire corpus. In this case
imprecise results are not acceptable.
</p>
<p>We explore the use of probabilistic models in order to help sift
through large numbers of results and prioritize them by decreasing
order of likelihood. We apply this to the computation of links between
over 10,000 Android applications with our PRIMO tool. PRIMO is able to
compute links between various applications as computed by IC3 (see
below). It can also compute the probability that these links are true
positives.
</p>
<p>For information on PRIMO, please visit
<a href="http://siis.cse.psu.edu/primo/">siis.cse.psu.edu/primo</a>.
</p>
<h3>COAL</h3>
<p>Many program analyses require statically inferring the possible
values of object variables. However, current approaches either do not
account for correlations between object fields or do so in an ad hoc
manner. The COAL project enables the specification and solution of
these problems in a principled way. The project includes a language
that is used to describe the classes of the objects whose value should
be inferred. It also includes a solver, which computes the object
values.
</p>
<p>The COAL language allows easy specification of composite constant
propagation problems. Our COAL solver takes as inputs a COAL
specification and the code that needs to be analyzed and automatically
outputs the value of the fields of the requested variables. Note that
in programs where there are several possible values for a given object,
the COAL solver infers all possible values, taking into account the
correlations between the fields on different execution paths.
</p>
<p>For information about COAL, please visit
<a href="http://siis.cse.psu.edu/coal/">siis.cse.psu.edu/coal</a>.
</p>
<h3>IC3</h3>
<p>Many threats present in smartphones are the result of interactions
between application components, not just artifacts of single
components. For example, information may flow between components in an
unsafe manner. A component in an application may retrieve a user's
location data or contacts. It may subsequently send the sensitive
private information to a component in another application. The
receiving component may then leak the sensitive information to the
network, to an untrusted third party.
</p>
<p>Using COAL, we build IC3, a tool for inferring ICC with
significantly better precision than Epicc. Unlike Epicc, it models all
ICC primitives.
</p>
<p>For information about IC3, please visit
<a href="http://siis.cse.psu.edu/ic3/">siis.cse.psu.edu/ic3</a>.
</p>
<h3>Epicc</h3>
<p>Epicc was our initial tool for inferring ICC in Android
applications. It paved the way for the idea of reducing the inference
of object values to an Interprocedural Distributive Environment (IDE)
data flow problem.
</p>
<p>For information regarding obtaining and using Epicc, please visit
<a href="http://siis.cse.psu.edu/epicc/">siis.cse.psu.edu/epicc</a>.
<h3>Dare</h3>
<p>Dare is a tool that retargets Android applications running on the Dalvik
Virtual Machine to traditional Java Virtual Machine .class files. These .class files can then be
processed by existing Java tools, including decompilers. Thus, Android
applications can be analyzed using a vast range of techniques developed for
traditional Java applications. Dare replaces ded as a retargeting tool: it
is more accurate, more efficient, more powerful and can even handle cases
where the input code is unverifiable.
</p>
<p>Dare was awarded the Best Artifact Award at the 20th International Symposium
on the Foundations of Software Engineering (FSE), recognizing its value as a
significant and high-quality tool. For more information, you can read the
paper "Retargeting Android Applications to Java Bytecode" by Octeau et al.,
published in the proceedings of the 20th International Symposium on the
Foundations of Software Engineering (FSE). For downloads, see the
<a href="http://siis.cse.psu.edu/dare/">Dare page</a>.
</p>
<h3>ded</h3>
<p>Smartphone applications are frequently incompletely vetted, poorly isolated,
and installed by users without restraint. Smartphone research frequently needs
to understand how these applications behave. ded is a project which aims at
decompiling Android applications. The ded tool retargets Android applications
in .dex format to traditional .class files. These .class files can then be
processed by existing Java tools, including decompilers. Thus, Android
applications can be analyzed using a vast range of techniques developed for
traditional Java applications.
</p>
<p>
For information regarding obtaining and using ded, please visit
<a href="http://siis.cse.psu.edu/ded/">siis.cse.psu.edu/ded</a>.
</p>
<br>
</div>
<div class="bott">
<table>
<tr> <td> </td> </tr>
</table>
</div>
</body>
</html>