-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathimplementazione.tex
523 lines (444 loc) · 26.2 KB
/
implementazione.tex
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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
\chapter{Implementazione di Dropper}
\label{cap:implementazione}
In questo capitolo si farà un'analisi dell'attuale stato di sviluppo
di Dropper.
\section{Modulo Core}
\subsection{Interazione con l'utente}
Attualmente Dropper si interfaccia con l'utente tramite alcune
funzioni della classe \lstinline{dropper}. Il costruttore di questa
classe riceve come argomento il percorso sul filesystem dove risiede
il file oggetto eseguibile da analizzare. Le operazioni di analisi
vengono avviate tramite la funzione \lstinline{analyze_all}. Una volta
che l'analisi è stata effettuata si può richiamare la funzione
\lstinline{build_spawn_shell_payload} che si occuperà di generare la
catena vera e propria. Anche se queste sono le uniche chiamate
essenziali per utilizzare Dropper l'utente ha a disposizione ulteriori
funzioni:
\begin{itemize}
\item \lstinline{set_can_control_fd} setta il file descriptor
controllato dall'utente (-1 se nessun file descriptor può essere
controllato)
\item \lstinline{add_shared_object} permette di analizzare un oggetto
che rappresenti una libreria dinamica. Dropper ricava da questo file
gli offset relativi tra gli indirizzi delle funzioni della libreria
\item \lstinline{set_function_for_address_resolving} indica la
funzione di riferimento da utilizzare nell'applicazione di tecniche
che ricavino l'indirizzo di funzioni casualizzate in memoria
partendo da valori nella GOT table (vedi sez. \ref{sec:expl}). La
funzione indicata dev'essere già stata richiamata almeno una volta
al momento dell'esecuzione della catena
\item \lstinline{set_writeable_area} imposta l'indirizzo dell'area di
memoria dove effettuare operazioni di scrittura. Di default questo
valore è impostato all'indirizzo di caricamento in memoria della
sezione \lstinline{.data}
\item \lstinline{set_cmd} setta il comando da eseguire sulla macchina
bersaglio una volta che l'exploit ha avuto successo
\end{itemize}
Quando il file eseguibile è stato analizzato e le informazioni
necessarie impostate il metodo \lstinline{build_spawn_shell_payload}
cerca di generare una catena che avvia il comando impostato.
\subsection{Analisi degli import}
Se una funzione esterna viene utilizzata dal programma, anche se il
suo indirizzo reale viene casualizzato, sarà presente un elemento
relativo a quella funzione all'interno della Procedure Linkage
Table. Questo elemento, ammesso che il binario non sia stato compilato
come indipendente dalla posizione in memoria (PIE), ha una posizione
nota. Possiamo quindi ritornare al suo indirizzo per emulare la
chiamata a quella funzione (return-to-plt). Nella GOT invece ogni
elemento inizialmente, e quindi anche staticamente nel file, contiene
l'indirizzo dell'istruzione successiva nell'elemento della PLT
relativo alla stessa funzione. Per ogni funzione la rilocazione
associata, nella sezione \lstinline{.rel.plt}, contiene nel campo
\lstinline{r_offset} l'indirizzo dell'elemento nella GOT table. A
partire da quest'ultimo, per le considerazioni appena fatte, può
essere ricavato l'indirizzo dell'elemento nella PLT. Gli indirizzi del
relativo elemento della GOT e di quello nella PLT vengono ricavati per
ogni funzione utilizzata dal file oggetto eseguibile nel metodo
\lstinline{get_imports}.
\subsection{Costruzione della catena}
Attualmente il modulo Core per prima cosa cerca di scrivere in un'area
di memoria scrivibile i dati ai quali punteranno gli argomenti
dell'invocazione della funzione \lstinline{execve}. Nel caso
quest'area di memoria non viene specificata dall'utente viene
utilizzato l'indirizzo di caricamento in memoria della sezione
\lstinline{.data}. Gli argomenti e i dati veri e propri vengono creati
dal modulo partendo dal comando che si è deciso di eseguire sulla
macchina (nella funzione \lstinline{payload_execve_args}). Se si può
controllare un file descriptor Core utilizza la funzione
\lstinline{read} per scrivere in memoria gli argomenti di
\lstinline{execve}, come descritto in \ref{sec:arc:core}. Per fare
questo viene utilizzato il metodo \lstinline{get_ret_func_chunk} del
modulo Gadget il quale ci consente di creare una catena che
richiami una funzione di cui si conosce l'indirizzo. È compito poi
dell'utente fare in modo che al momento della chiamata di questa
funzione il file descriptor indicato si trovi nello stato giusto in
modo da restituire i valori calcolati dal modulo. I valori da inserire
nel flusso del file descriptor vengono ricavati dall'utente attraverso
il parametro \lstinline{fd_payload} di dropper.
%%TODO
%%Esempio?
Attualmente è implementata una seconda strategia nel caso non sia
possibile richiamare la funzione \lstinline{read} e/o non si controlli
nessun file descriptor. Essa consiste nell'utilizzare una serie di
gadget che possano spostare valori dallo stack in una locazione di
memoria arbitraria. Per costruire una catena del genere si chiama la
funzione \lstinline{build_memory_write} del modulo Gadgets che prende
come argomenti l'indirizzo della memoria dove scrivere i
dati. Solitamente, come vedremo in \ref{sec:memorystore}, le catene
generate in questo modo tendono ad essere piuttosto lunghe.
%%TODO inserire strategie non implementate?
Per quanto riguarda la seconda fase, la chiamata della funzione, sono
state implementate due strategie. La prima nel caso \lstinline{execve}
sia presente all'interno delle funzioni utilizzate dal programma. In
questo caso la generazione della parte restante della catena è banale
e, come visto nel paragrafo precedente, viene costruita dalla funzione
\lstinline{get_ret_func_chunk} del modulo Gadgets. Più
interessante è il caso in cui il file oggetto eseguibile non utilizzi
questa funzione.
Infatti in questo Dropper cerca di far costruire al modulo Dropper una
catena in grado di modificare il valore della Global Offset Table in
loco, in modo da effettuare una tecnica di tipo \emph{got patching}
(vedi \ref{sec:expl}). Il modulo Gadgets espone il metodo
\lstinline{build_mem_add} che si occupa dei dettagli
implementativi di questo tipo di catena. Viene chiamato dal modulo
Core con i seguenti parametri:
\begin{itemize}
\item l'indirizzo di memoria dove eseguire la somma: l'indirizzo
dell'elemento della GOT da ``patchare''. La funzione viene
indicata dall'utente tramite la funzione
\lstinline{set_function_for_address_resolving} e l'indirizzo viene
ricavato durante la fase dell'analisi degli import
\item l'addendo: l'offset relativo tra la funzione
utilizzata come base e quella voluta, questo valore viene
eventualmente ricavato dai file oggetto condivisi forniti a
Dropper tramite il metodo \lstinline{add_shared_object}
\item il valore di base: l'offset che la funzione di base ha
all'interno del file oggetto condiviso della libreria, anch'esso
ottenuto analizzando un file indicato con la funzione
\lstinline{add_shared_object}. Come vedremo questo rende possibile
utilizzare una tecnica di tipo got patching anche quando le
tipologie di gadget disponibili non sono ideali al prezzo di
sacrificare un'affidabilità del 100\% (vedi
sez. \ref{sec:arithmeticstore})
\end{itemize}
La classe inoltre contiene alcuni metodi per il salvataggio dei dati
relativi ai gadget su disco, questo perché l'analisi di eseguibili
molto grandi può durare diversi minuti. Al loro interno questi metodi
utilizzano la libreria \lstinline{pickle} per la serializzazione degli
oggetti.
\section{Modulo Gadgets}
Questo modulo, come descritto nel capitolo dedicato all'architettura,
estrapola e cataloga i gadget presenti nel binario in esame ed espone
i metodi di creazione delle catene per l'esecuzione di diverse
funzioni. Le catene vengono costruite arrangiando i gadget disponibili
e collaborando con il modulo Payload che si occupa della generazione
del payload vero e proprio. Attualmente il modulo mette a disposizione
i seguenti metodi per la generazione delle catene:
\begin{itemize}
\item \lstinline{get_stack_slide_chunk}: consente di aggiungere un
valore arbitrario al registro dello stack, questo tipo di catene
ci consente ad esempio di ``saltare'' gli argomenti di una
funzione sullo stack e passare al gadget successivo
\item \lstinline{get_ret_func_chunk}: restituisce una catena che
richiami una funzione. Riceve come parametri di ingresso gli
argomenti da passare alla funzione e l'indirizzo della funzione
stessa
\item \lstinline{get_memory_add_chunk}: restituisce una catena che
esegue un operazione di addizione in una locazione di memoria
arbitraria
\item \lstinline{get_memory_store_chunk}: restituisce una catena che
scrive in memoria valori arbitrari
\item \lstinline{get_ccf_chunk}: restituisce un chunk che azzeri il
carry flag
\end{itemize}
Le tipologie di gadget utilizzate per la costruzione di queste catene
sono descritte nella parte restante di questo capitolo.
Fondamentale per poter utilizzare un gadget è poter controllare i
registri coinvolti nelle sue operazioni, per questo motivo la prima
analisi che viene condotta una volta ottenuta la lista dei gadget è la
selezione di quelli che ci consentono di controllare i registri. La
ricerca dei gadget viene effettuata in tutte le sezioni che vengono
caricate in memoria e marcate come eseguibili. Si è deciso di separare
il modulo in diverse sottoclassi, ognuna delle quali contiene la
logica per la selezione e l'utilizzo di un particolare tipo di gadget.
\subsection{Gadget per l'impostazione dei registri}
La logica e le strutture dati utilizzate per la selezione e la
gestione dei gadget utilizzati per l'impostazione dei registri è
contenuta nella classe \lstinline{RegSet}. Il metodo
\lstinline{_analyze_gadget} riceve come argomento in ingresso un
gadget e, nel caso esso possa essere utilizzato per l'impostazione di
registri, viene aggiunto nelle strutture dati interne alla classe. La
classe espone il metodo \lstinline{get_chunk} che ritorna una catena
che imposta i registri in modo da riflettere le coppie registro/valore
del dizionario preso come argomento. Attualmente solo gadget che
contengono istruzioni di tipo \lstinline{pop reg} vengono considerati
come potenziali candidati per l'impostazione di registri.
L'analisi avviene tramite una simulazione istruzione per
istruzione. Se l'istruzione attuale è di tipo \lstinline{pop reg}
allora si memorizza il nome del registro e l'offset tra il valore
attuale dello stack e quello all'inizio della simulazione. Questo ci
consente di conoscere dove posizionare il valore da impostare nel
registro al momento della generazione del payload. Durante la
simulazione si controlla anche che le istruzioni che non sono del tipo
\lstinline{pop reg} non eseguano operazioni di lettura o scrittura
sulla memoria. Questo ci consente di scartare già in questa fase i
gadget che presentano effetti secondari. Dopo la fase di analisi
quindi avremo, per ogni gadget, la lista dei registri che possono
essere impostati insieme all'ordine e alla posizione con cui vengono
prelevati dallo stack.
La funzione \lstinline{get_chunk} invece restituisce una catena che
consente di impostare l'insieme dei registri che riceve in
ingresso. Dato che un gadget potrebbe impostare più di un registro, la
scelta dei gadget che andranno a comporre questa catena è riducibile
ad un problema di \emph{set covering}. È preferibile che il payload
generato dalla catena sia il più piccolo possibile. La lunghezza della
catena è influenzata sia dal numero di gadget utilizzati, sia dal
padding che è necessario inserire nell'utilizzo di ogni gadget per via
delle operazioni che esso effettua sul registro dello
stack. Attualmente per trovare la catena viene utilizzato un algoritmo
greedy che scorre i registri da ``coprire'' e, se il registro non è
già coperto da un gadget inserito nella catena, sceglie il gadget che
lo copre e che necessita del minor padding possibile. Se l'aggiunta di
un gadget ne rende superfluo uno già presente nei candidati
quest'ultimo viene rimosso. La soluzione trovata con quest'algoritmo
non è ottima. Nella sezione \ref{sec:pddl} è descritto un primo
approccio per l'utilizzo di planner nella ricerca di una sequenza
ottima.
\subsection{Gadget per la scrittura in memoria}
\label{sec:memorystore}
La logica e le strutture dati per gestire i gadget che ci consentono
di scrivere in memoria si trovano nella classe
\lstinline{MemoryStore}.
Durante la prima classificazione la classe
\lstinline{GadgetClassifier} del framework BARF verifica se a seguito
di alcune simulazioni un valore presente in un registro (denominato
sorgente) viene scritto in una locazione di memoria il cui indirizzo
corrisponde al valore di un registro (denominato destinazione) sommato
ad un eventuale offset.
Ogni volta che questa condizione viene verificata il gadget viene
aggiunto alla categoria StoreMemory. È da notare che la condizione di
cui sopra potrebbe verificarsi per più coppie di registri nello stesso
gadget, per ognuna di queste viene creato un oggetto gadget di tipo
StoreMemory e aggiunto alla categoria. La classe parte da questi
gadget per procedere alla fase di verifica e validazione.
Innanzitutto se il registro di destinazione è il registro dello stack
il gadget viene scartato. Questo fa in modo che non vengano presi in
considerazione i gadget con istruzioni tipo \lstinline{push reg}.
Questi gadget infatti, solitamente non consentono di scrivere in una
regione arbitraria della memoria, oltre a complicare la gestione dello
schema dello stack. Dopo di che vengono scartati anche i gadget che
hanno come registro di destinazione \lstinline{rip} o
\lstinline{eip}. Infatti essendo questo registro fisso rispetto
all'istruzione che lo esegue neanche questi gadget ci consentono di
scrivere in una posizione arbitraria di memoria.
Dopo di che, utilizzando le metodologie descritte in
\ref{sec:verifica_validazione}, il gadget viene scartato se non si
possono controllare i registri sorgente e destinazione, se ne verifica
e valida la generalità e ci si assicura che il gadget non presenti
effetti secondari. Nella verifica degli effetti secondari si controlla
che non ci siano scritture al di fuori della locazione scelta e dello
stack.
Il metodo \lstinline{get_chunk} invece prende come argomenti un
indirizzo in memoria e una stringa e restituisce una catena che scrive
la stringa in memoria partendo da quell'indirizzo. Il metodo quindi
espone un livello d'astrazione più alto al modulo che la utilizza e,
normalmente, vi è bisogno di più iterazioni dell'esecuzione del gadget
per ottenere la scrittura desiderata. Il metodo, infatti, oltre a
scegliere uno dei gadget disponibili calcola il numero di queste
iterazioni necessarie per la scrittura dei valori. Per ogni iterazione
poi utilizza una modellazione logica unita ad un risolutore SMT per
ottenere i valori dei registri sorgente e destinazione corretti. Anche
se si potrebbero utilizzare il valore di offset ottenuto durante la
fase di catalogazione del gadget utilizzare il risolutore ci permette
di utilizzare anche gadget i cui effetti secondari modifichino la
locazione di memoria in maniera indipendente dagli altri
registri. Sempre per ogni iterazione, si utilizza la classe
\lstinline{regset} per ottenere una catena che setti i registri a quei
valori, e la si concatena a sua volta al gadget che si sta utilizzando
per scrivere in memoria. Viene restituita la concatenazione delle
catene create per ogni iterazione, che verosimilmente scriverà in
memoria, partendo dall'indirizzo indicato i valori in ingresso.
\subsection{Gadget per la operazioni aritmetiche in
memoria}
\label{sec:arithmeticstore}
La logica e le strutture dati per la gestione dei gadget che ci
consentono di scrivere in memoria risiedono nella classe
\lstinline{aritmeticmemorystore}.
Anche in questo caso si parte dai gadget classificati dal framework
BARF, ma appartenenti, per l'appunto, alla categoria Arithmetic Memory
Store. Un gadget viene inserito in questa categoria se, dopo alcune
simulazioni del gadget, una locazione di memoria viene modificata e
come valore finale riflette il risultato di un'operazione aritmetica
binaria tra il valore precedente di quella locazione e il valore
iniziale contenuto in un registro. Inoltre si individua un registro
che potrebbe essere usato dal gadget come indirizzo della locazione di
memoria (insieme ad un eventuale offset). Dato che la simulazione
viene ripetuta più volte i falsi positivi vengono ridotti. È possibile
che un gadget esibisca il comportamento di cui sopra più di una volta,
anche in questo caso vengono creati diversi oggetti di tipo Arithmetic
Memory Store. La verifica di questi gadget procede in maniera molto
simile a quella dei gadget per la scrittura della memoria.
Tuttavia un'attenzione particolare va posta nell'analisi dei gadget
che utilizzano un'operazione di addizione che considerano il valore di
riporto (ad esempio adc su architettura intel). Questi gadget possono
rilevarsi molto utili. Spesso infatti sono disponibili solo gadget
aritmetici che ci consentono di aggiungere un byte per
volta. Effettuare un'operazione di got patching (vedi
sez. \ref{sec:expl}) un byte per volta senza considerare i valori di
riporto tra un byte e il successivo può portare ad un risultato errato
dell'operazione che si sta effettuando. Per poter permettere la
catalogazione di questo tipo di gadget, si è dovuto applicare una
piccola patch al framework per permetterci di poter controllare in
qualche modo il contesto dei registri che utilizza durante le
simulazioni per la classificazione. Questo ci ha permesso di impostare
durante le simulazioni il valore del carry flag a zero, facendo in
modo che la procedura di catalogazione non scarti i gadget di questo
tipo. Anche le verifiche tramite un risolutore SMT impongono che il
carry flag abbia valore zero. In più viene aggiunta una seconda coppia
di modellazioni SMT con le quali si verifica se il gadget in esame
utilizza il carry flag nell'operazione e se a seguito di un'operazione
che sicuramente generi un valore di riporto, il carry flag al termine
dell'esecuzione del gadget abbia valore uno. Questo ci dà la certezza
rispettivamente che il gadget va ad utilizzare il carry flag nelle
operazioni di addizione e che le operazioni successive all'interno del
gadget non vadano ad influenzare il carry flag.
Come detto sopra, per costruire una catena che ci consente di
aggiungere un valore arbitrario ad una locazione di memoria
arbitraria, bisogna avere a disposizione o gadget aritmetici la cui
dimensione dell'operazione sia di almeno un byte più grande
dell'addendo o un gadget che, per l'appunto, consenta di eseguire
operazioni utilizzando i valori di ritorno. In questo secondo caso
però bisogna anche concatenare, se è disponibile, un gadget che abbia
come effetto quello di azzerare il carry flag, da inserire prima
dell'operazione. La logica per la ricerca di questo tipo di gadget è
presente nella classe \lstinline{ClearCarryFlag}. È da notare che se
questo tipo di gadget non fosse presente la catena generata potrebbe
non avere l'esito sperato, tuttavia è presumibile che in molti tipi di
exploit il carry flag abbia sempre lo stesso valore all'inizio
dell'esecuzione della catena. La sottrazione quindi di un'unità al
primo byte dell'addendo dovrebbe essere sufficiente per generare una
catena corretta.
Se non sono disponibili né un un gadget che consenta di aggiungere
abbastanza byte per volta né un gadget che effettua operazioni
considerando il valore di riporto è tuttavia possibile generare una
catena con alte probabilità di successo. Infatti l'indirizzo di
memoria nel quale viene caricato il file oggetto condiviso della
libreria, nonostante sia casualizzato, dev'essere allineato in memoria
al valore specificato nel parametro \lstinline{p_align} all'interno
del Program Header. Questo comporta che un certo numero di bit meno
significativi dell'indirizzo di una funzione non cambino da
un'esecuzione all'altra. Solitamente sono i 21bis meno significativi,
e l'offset tra due funzioni nella libc solitamente è tre byte. Questo
fa si che si può calcolare il valore di riporto per i primi due
byte. Solo il valore di riporto dell'ultimo byte (di cui conosciamo
solo la parte meno significativa) risulterebbe casuale, facendo si che
si possano generare catene con probabilità di successo pari almeno al
50\%.
\section{Modulo Payload}
Questo modulo si occupa di generare a partire da una lista ordinata di
uno o più gadget una stringa binaria di dati da iniettare nello stack
del file oggetto eseguibile esaminato, denominata Payload. La
preparazione del payload varia rispetto al gadget per il quale si sta
creando il chunk e può consistere nel solo indirizzo del gadget, o in
schemi più complicati come indirizzi di funzioni più relativi
argomenti o a valori da trasferire dallo stack ai registri. Ogni
classe che si occupa della generazione di un particolare tipo di chunk
ha le informazioni necessarie per permettere al chunk stesso di essere
concatenato ad altri chunk per generarne un altro, anch'esso a sua
volta concatenabile, che rappresenti i chunk di partenza. Per
permettere questa concatenazione ogni chunk deve presentare le
seguenti informazioni:
%3201899105
\begin{itemize}
\item L'indirizzo che deve trovarsi sullo stack al momento
dell'esecuzione dell'istruzione ret del gadget precedente
\item In quale posizione del payload inserire l'indirizzo del gadget
successivo
\item La dimensione degli indirizzi nell'architettura considerata
\end{itemize}
Le classi che modellano i vari tipi di chunk hanno tutti un metodo,
\lstinline{get_payload}, che restituisce il payload del chunk di
riferimento (escluso l'indirizzo del gadget stesso). Quando due gadget
vengono concatenati per generare un chunk più generico (nel metodo
\lstinline{PayloadChunk.get_general_chunk}), l'indirizzo di ogni chunk
viene inserito nella posizione indicata dal chunk precedente. Nel
momento che si richiede il payload vero e proprio (attraverso il
metodo \lstinline{PayloadChunk.chain}) oltre all'operazione di
concatenazione viene anche inserito l'indirizzo del primo gadget
all'inizio del payload.
%TODO spostare in implementazione attuale?
%% Questo avviene emulando tutti i gadgets, e nello stesso momento
%% parsando le istruzioni. Si tiene traccia, istruzione per istruzione,
%% di quanto si sia modificato il valore dello stack. Nel caso si
%% incontri un'istruzione del tipo pop reg, viene associato a quel
%% registro l'attuale differenza tra il valore dello stack relativamente
%% all'istruzione corrente e quello all'inizio della simulazione. A
%% questo punto abbiamo per ogni gadget una lista di registri e di offset
%% rispetto ai quali inserire il valore nello stack per inserire un
%% valore arbitrario nel relativo registro. Inoltre tramite la
%% simulazione si deduce la differenza tra il valore dello stack
%% all'inizio del gadget e quello alla fine. Questo valore dovrà essere
%% noto solitamente per tutti i gadget in quando ci permette di far
%% trovare al posto giusto l'indirizzo di ritorno del gadget lo che
%% succede nella catena. Nel caso il gadget non contenga nessuna
%% istruzione del tipo pop reg, questo viene scartato. Inoltre nella
%% simulazione viene tenuta traccia degli indirizzi di memoria letti e/o
%% scritti. Nel caso vi sia scrittura nella memoria o lettura da una zona
%% di memoria non riconducibile all'area relativa allo stack il gadget
%% viene scartato.
%% La semantica potrebbe essere poi verificata trasformando le istruzioni
%% del gadget in formule smt, verifcando che la semantica e i valori
%% estratti non siano dipendendi dai valori di ingresso, e quindi
%% relativi solo alla simulazione effettuata. In pspecial modo è possibile
%% che il valore dello stack venga modificato utilizzando un valore di un
%% registro. TODO
%% La catena dei gadget generata da dROPper deve, una volta
%% iniettata nello stack del processo in esecuzione, poter eseguire un
%% comando arbitrario sulla macchina in cui è in corso l'esecuzione del
%% programma. La catena generata deve funzionare anche nel caso che gli
%% indirizzi in memoria delle librerie utilizzate da programma siano
%% stati casualizzati (ASRL) e che nè lo stack nè alcuna regione
%% scrivibile sia eseguibile (NX). La strategia da utilizzare dipende dal
%% binario utilizzato e da che tipo di controllo abbiamo sui dati di
%% ingresso del programma. In ogni caso lo schema principale, con alcune
%% varianti che analizzeremo in seguito, si può dividere in due fasi
%% principali: (a) preparare gli argomenti per eseguire una chiamata ad
%% una funzione di libreria che ci consenta di eseguire un comando
%% arbitrario e (b) eseguire quella funzione al fine si eseguire il
%% comando voluto. Le strategie per arrivare alla concretizzazione di
%% queste due fasi dipendono dal file oggetto eseguibile che si sta
%% analizzando che può presentare scenari relativamente semplici, in cui
%% ad esempio il programma utilizza già le chiamate a funzioni
%% necessarie, permettendoci di utilizzare \emph{return-to-plt} sia a
%% scenari più complessi, dove l'indirizzo delle funzioni necessarie
%% viene ottenuto durante l'esecuzione partendo dagli indirizzi presenti
%% nella Global Offset Table.
%% Dropper inizia ad analizzare il binario affidandosi al framework BARF
%% per l'estrazione e una prima cataloghizzazione dei gadget. Le
%% categorie in cui il framework suddivide i gadget sono quelle indicate
%% in[]:
%% \begin{itemize}
%% \end{itemize}
%% \section{Implementazione attuale}
%% \subsection{dropper}
%% Dropper legge dal file le sezioni
%% \lstinline{.rel.plt}, \lstinline{.dynsym},\lstinline{.got} e
%% \lstinline{.got.plt}.
%% analizza
%% poi la sezione ``.data'', se non viene specificato diversamente
%% dall'utente verrà utilizzato l'indirizzo in memoria di questa sezione
%% come area di memoria dove poter scrivere dati. Questo ci permette di
%% avere una posizione nota (l'indirizzo in memoria di ``.data.'' non è
%% casualizzato) dove poter scvrivere gli argomenti delle funzioni che
%% andremo ad utilizzare
%% TODO :
%% # verificare i gadget di tipo regset
%% # trovare i tipi regset e modellare la memoria (utilizzando > e < per
%% segnare le aree di memoria scrivibili e le aree di memoria leggibili)
%% Una prima
%% possibiltà è quella di utilizzare delle sequenze di gadget che ci
%% consentato di modificare un valore in memoria aggiungendoci un
%% addendo. In questo modo è possibile addizionare l'offset noto nell got
%% table, e successivamente fare un ret-to-plt. Il valore presente nella
%% got table adesso punterà alla funzione voluta. Per utilizzare questa
%% tecnica devono essere soddisfatte le seguenti precondizioni: