|
1 |
| -# Explode-js example |
2 |
| - |
3 |
| -Considering the example program in the file `exec.js`: |
4 |
| - |
5 |
| -```javascript |
6 |
| -let exec = require('child_process').exec; |
7 |
| - |
8 |
| -module.exports = function f(source) { |
9 |
| - if (Array.isArray(source)) { |
10 |
| - return exec(source.join(' ')); |
11 |
| - } |
12 |
| - return exec(source); |
13 |
| -}; |
14 |
| -``` |
15 |
| - |
16 |
| -Notice that the function `f` receives a `source` parameter and, if it is an |
17 |
| -array, it joins its elements with a space and executes the command. |
18 |
| -Otherwise, it executes the command directly. Function `f` is vulnerable to |
19 |
| -two vulnerabilities of command injection depending on the input. |
20 |
| - |
21 |
| -Explode.js will ask graph.js if it is able to identify the vulnerabilities |
22 |
| -in the function `f`. Graph.js, will output the following taint summary: |
23 |
| - |
24 |
| -```sh |
25 |
| -$ graphjs --with-types -f exec.js -o _results/run |
26 |
| -... |
27 |
| -$ cat _results/run/taint_summary.json |
28 |
| -[ |
29 |
| - { |
30 |
| - "type": "VFunExported", |
31 |
| - "filename": ... |
32 |
| - "vuln_type": "command-injection", |
33 |
| - "sink": "return exec(source.join(' '));", |
34 |
| - "sink_lineno": 5, |
35 |
| - "source": "module.exports", |
36 |
| - "tainted_params": [ |
37 |
| - "source" |
38 |
| - ], |
39 |
| - "params_types": { |
40 |
| - "source": { |
41 |
| - "_union": [ |
42 |
| - "array", |
43 |
| - "string" |
44 |
| - ] |
45 |
| - } |
46 |
| - }, |
47 |
| - "call_paths": [ |
48 |
| - { |
49 |
| - "type": "Call", |
50 |
| - "fn_name": "119.f-o24", |
51 |
| - "fn_id": "82", |
52 |
| - "source_fn_id": "82" |
53 |
| - } |
54 |
| - ] |
55 |
| - }, |
56 |
| - { |
57 |
| - "type": "VFunExported", |
58 |
| - "filename": ... |
59 |
| - "vuln_type": "command-injection", |
60 |
| - "sink": "return exec(source);", |
61 |
| - "sink_lineno": 7, |
62 |
| - "source": "module.exports", |
63 |
| - "tainted_params": [ |
64 |
| - "source" |
65 |
| - ], |
66 |
| - "params_types": { |
67 |
| - "source": { |
68 |
| - "_union": [ |
69 |
| - "array", |
70 |
| - "string" |
71 |
| - ] |
72 |
| - } |
73 |
| - }, |
74 |
| - "call_paths": [ |
75 |
| - { |
76 |
| - "type": "Call", |
77 |
| - "fn_name": "119.f-o24", |
78 |
| - "fn_id": "82", |
79 |
| - "source_fn_id": "82" |
80 |
| - } |
81 |
| - ] |
82 |
| - } |
83 |
| -] |
84 |
| -``` |
85 |
| - |
86 |
| -Importantly, notice that the summary contains two vulnerabilities with the |
87 |
| -same source, but with different sinks and parameters. The first vulnerability |
88 |
| -is related to the case where the `source` parameter is an array, and the second |
89 |
| -vulnerability is related to the case where the `source` parameter is a string. |
90 |
| - |
91 |
| -To confirm the vulnerabilities, Explode.js will execute explode-js like this: |
92 |
| - |
93 |
| -```sh |
94 |
| -$ explode-js run --filename exec.js _results/run/taint_summary.json |
95 |
| -── PHASE 1: TEMPLATE GENERATION ── |
96 |
| -✔ Loaded: _results/run/taint_summary.json |
97 |
| -⚒ Generating 4 template(s): |
98 |
| -├── 📄 ./symbolic_test_0.js |
99 |
| -├── 📄 ./symbolic_test_1.js |
100 |
| -├── 📄 ./symbolic_test_2.js |
101 |
| -├── 📄 ./symbolic_test_3.js |
102 |
| - |
103 |
| -── PHASE 2: ANALYSIS & VALIDATION ── |
104 |
| -◉ [1/4] Procesing ./symbolic_test_0.js |
105 |
| -├── Symbolic execution output: |
106 |
| -Exec failure: source0 |
107 |
| -├── Symbolic execution stats: clock: 0.274821s | solver: 0.001687s |
108 |
| -├── ⚠ Detected 1 issue(s)! |
109 |
| -│ ├── ↺ Replaying 1 test case(s) |
110 |
| -│ │ ├── 📄 [1/1] Using test case: ./symbolic_test_0/test-suite/witness-0.json |
111 |
| -│ │ │ ├── Node exited with 0 |
112 |
| -│ │ │ └── ✔ Status: Success (created file "./success") |
113 |
| -◉ [2/4] Procesing ./symbolic_test_1.js |
114 |
| -├── Symbolic execution output: |
115 |
| -Exec failure: source |
116 |
| -├── Symbolic execution stats: clock: 0.273059s | solver: 0.002672s |
117 |
| -├── ⚠ Detected 1 issue(s)! |
118 |
| -│ ├── ↺ Replaying 1 test case(s) |
119 |
| -│ │ ├── 📄 [1/1] Using test case: ./symbolic_test_1/test-suite/witness-1.json |
120 |
| -│ │ │ ├── Node exited with 0 |
121 |
| -│ │ │ └── ✔ Status: Success (created file "./success") |
122 |
| -◉ [3/4] Procesing ./symbolic_test_2.js |
123 |
| -├── Symbolic execution output: |
124 |
| -Exec failure: source0 |
125 |
| -├── Symbolic execution stats: clock: 0.269539s | solver: 0.003842s |
126 |
| -├── ⚠ Detected 1 issue(s)! |
127 |
| -│ ├── ↺ Replaying 1 test case(s) |
128 |
| -│ │ ├── 📄 [1/1] Using test case: ./symbolic_test_2/test-suite/witness-2.json |
129 |
| -│ │ │ ├── Node exited with 0 |
130 |
| -│ │ │ └── ✔ Status: Success (created file "./success") |
131 |
| -◉ [4/4] Procesing ./symbolic_test_3.js |
132 |
| -├── Symbolic execution output: |
133 |
| -Exec failure: source |
134 |
| -├── Symbolic execution stats: clock: 0.274064s | solver: 0.004895s |
135 |
| -├── ⚠ Detected 1 issue(s)! |
136 |
| -│ ├── ↺ Replaying 1 test case(s) |
137 |
| -│ │ ├── 📄 [1/1] Using test case: ./symbolic_test_3/test-suite/witness-3.json |
138 |
| -│ │ │ ├── Node exited with 0 |
139 |
| -│ │ │ └── ✔ Status: Success (created file "./success") |
140 |
| -``` |
141 |
| - |
142 |
| -The output show that explode-js first created two symbolic tests, `symbolic_test_0_0.js` |
143 |
| -and `symbolic_test_1_0.js`, and then executed explode-js with each of them. The output |
144 |
| -shows that both tests found a problem, and subsequently during the replaying phase |
145 |
| -where the symbolic tests are executed with the concrete models generated in |
146 |
| -`_results/run/symbolic_test_0_0/test-suite/witness-0.js` and `_results/run/symbolic_test_1_0/test-suite/witness-1.js`, |
147 |
| -respectively, each being able to create a file named `success`. This confirms that |
148 |
| -the vulnerabilities are present in the function `f`. |
149 |
| - |
150 |
| -Below we analyse the directory structure created by explode-js: |
151 |
| - |
152 |
| -```sh |
153 |
| -$ tree _results |
154 |
| -_results |
155 |
| -└── run |
156 |
| - ├── 20250311T103601 |
157 |
| - │ ├── exec.js |
158 |
| - │ ├── report.json |
159 |
| - │ ├── symbolic_test_0 |
160 |
| - │ │ ├── literal_1.js |
161 |
| - │ │ ├── report.json |
162 |
| - │ │ └── test-suite |
163 |
| - │ │ ├── witness-0.json |
164 |
| - │ │ ├── witness-0.json.stderr |
165 |
| - │ │ ├── witness-0.json.stdout |
166 |
| - │ │ └── witness-0.smtml |
167 |
| - │ ├── symbolic_test_0.js |
168 |
| - │ ├── symbolic_test_1 |
169 |
| - │ │ ├── literal_1.js |
170 |
| - │ │ ├── report.json |
171 |
| - │ │ └── test-suite |
172 |
| - │ │ ├── witness-1.json |
173 |
| - │ │ ├── witness-1.json.stderr |
174 |
| - │ │ ├── witness-1.json.stdout |
175 |
| - │ │ └── witness-1.smtml |
176 |
| - │ ├── symbolic_test_1.js |
177 |
| - │ ├── symbolic_test_2 |
178 |
| - │ │ ├── literal_1.js |
179 |
| - │ │ ├── report.json |
180 |
| - │ │ └── test-suite |
181 |
| - │ │ ├── witness-2.json |
182 |
| - │ │ ├── witness-2.json.stderr |
183 |
| - │ │ ├── witness-2.json.stdout |
184 |
| - │ │ └── witness-2.smtml |
185 |
| - │ ├── symbolic_test_2.js |
186 |
| - │ ├── symbolic_test_3 |
187 |
| - │ │ ├── literal_1.js |
188 |
| - │ │ ├── report.json |
189 |
| - │ │ └── test-suite |
190 |
| - │ │ ├── witness-3.json |
191 |
| - │ │ ├── witness-3.json.stderr |
192 |
| - │ │ ├── witness-3.json.stdout |
193 |
| - │ │ └── witness-3.smtml |
194 |
| - │ ├── symbolic_test_3.js |
195 |
| - │ └── taint_summary.json |
196 |
| - ├── graph |
197 |
| - │ ├── dependency_graph.txt |
198 |
| - │ ├── exec.js |
199 |
| - │ ├── graph_stats.json |
200 |
| - │ ├── graph.svg |
201 |
| - │ ├── nodes.csv |
202 |
| - │ └── rels.csv |
203 |
| - ├── run |
204 |
| - │ ├── neo4j_import.txt |
205 |
| - │ ├── neo4j_start.txt |
206 |
| - │ ├── neo4j_stop.txt |
207 |
| - │ └── time_stats.txt |
208 |
| - ├── taint_summary_detection.json |
209 |
| - └── taint_summary.json |
210 |
| - |
211 |
| -13 directories, 43 files |
212 |
| -``` |
213 |
| - |
214 |
| -The directory `_results/run/*` contains the symbolic tests and the directories |
215 |
| -`symbolic_test_0_0` and `symbolic_test_1_0` contain the result of the respective |
216 |
| -symbolic test. |
217 |
| - |
218 |
| -The `_results/run/*/symbolic_test_0_0/report.json` contains the symbolic |
219 |
| -execution summary of the first symbolic test: |
220 |
| - |
221 |
| -```sh |
222 |
| -$ cat _results/run/*/symbolic_test_0/report.json |
223 |
| -{ |
224 |
| - "filename": "./symbolic_test_0.js", |
225 |
| - "execution_time": 0.27482104301452637, |
226 |
| - "solver_time": 0.0016868114471435547, |
227 |
| - "solver_queries": 1, |
228 |
| - "num_failures": 1, |
229 |
| - "failures": [ |
230 |
| - { |
231 |
| - "type": "Exec failure", |
232 |
| - "sink": "source0", |
233 |
| - "pc": "(str.contains source0 \"`touch success`\")", |
234 |
| - "pc_path": "./symbolic_test_0/test-suite/witness-0.smtml", |
235 |
| - "model": { |
236 |
| - "data": { |
237 |
| - "model": { "source0": { "ty": "str", "value": "`touch success`" } } |
238 |
| - }, |
239 |
| - "path": "./symbolic_test_0/test-suite/witness-0.json" |
240 |
| - }, |
241 |
| - "exploit": { |
242 |
| - "success": true, |
243 |
| - "effect": "(created file \"./success\")" |
244 |
| - } |
245 |
| - } |
246 |
| - ] |
247 |
| -} |
248 |
| -``` |
249 |
| -
|
250 |
| -Observe that the symbolic execution summary shows that the symbolic test |
251 |
| -`symbolic_test_0.js` found a failure related to the sink "Exec" and that |
252 |
| -the symbolic expression `(#source0 : __$Str)` was responsible for triggering |
253 |
| -the failure. |
254 |
| - |
255 |
| -Furthermore, the report contains the information related to the confirmation |
256 |
| -of the respective failure in the `"exploit"` field. |
257 |
| -The `"model"` field shows the model generated by symbolic execution. Here, it is |
258 |
| -located at `_results/run/*/symbolic_test_0_0/test-suite/witness-0.js`. |
259 |
| -Inspecting the contents of the file: |
260 |
| - |
261 |
| -```sh |
262 |
| -$ cat _results/run/*/symbolic_test_0/test-suite/witness-0.json |
263 |
| -{ "model": { "source0": { "ty": "str", "value": "`touch success`" } } } |
264 |
| -``` |
265 |
| -
|
266 |
| -It shows that the a symbolic model with the assignment to the `#source0`, |
267 |
| -which is the a concrete assignment that triggers the vulnerability in the |
268 |
| -function `f`. |
269 |
| -
|
270 |
| -For reference, the `_results/run/*/symbolic_test_0_0.js` looks like this: |
271 |
| -
|
272 |
| -```sh |
273 |
| -$ cat _results/run/*/symbolic_test_0.js |
274 |
| -let exec = require('child_process').exec; |
275 |
| -
|
276 |
| -module.exports = function f(source) { |
277 |
| - if (Array.isArray(source)) { |
278 |
| - return exec(source.join(' ')); |
279 |
| - } |
280 |
| - return exec(source); |
281 |
| -}; |
282 |
| -
|
283 |
| -var esl_symbolic = require("esl_symbolic"); |
284 |
| -// Vuln: command-injection |
285 |
| -var source = [ esl_symbolic.string("source0") ]; |
286 |
| -module.exports(source); |
287 |
| -``` |
| 1 | +# Examples |
| 2 | + |
| 3 | +- [code-injection] |
| 4 | +- [command-injection] |
| 5 | +- [package-example] |
| 6 | +- [path-traversal] |
| 7 | +- [prototype-pollution] |
| 8 | + |
| 9 | +[code-injection]: ./code-injection |
| 10 | +[command-injection]: ./command-injection |
| 11 | +[package-example]: ./package-example |
| 12 | +[path-traversal]: ./path-traversal |
| 13 | +[prototype-pollution]: ./prototype-pollution |
0 commit comments