-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLdrpInitializeProcess.lmod
129 lines (104 loc) · 4.91 KB
/
LdrpInitializeProcess.lmod
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
LOADREL ntkrnlmp
DEFINE FILESIZE 500
INPUT HEADER FILESIZE as DOSHeader
P: NT_HEADER <- HEADER[HEADER.e_lfanew, sizeof _IMAGE_NT_HEADERS] as _IMAGE_NT_HEADERS
P: fileHdr <- NT_HEADER.FileHeader as _IMAGE_FILE_HEADER
P: optHdr <- NT_HEADER.OptionalHeader as _IMAGE_OPTIONAL_HEADER
P: imageEnd <- ADD optHdr.ImageBase optHdr.SizeOfImage
### Section alignment condition
### If SectionAlign < 0x1000, the image is mapped as is,
### using ImageBase and SizeOfImage only.
### Otherwise, each section is mapped at its own address
V1: UGE optHdr.SectionAlignment 0x1000
P: tlsDir <- optHdr.DataDirectory[72, 8] as _IMAGE_DATA_DIRECTORY
P: tlsDirEnd <- ADD tlsDir.VirtualAddress tlsDir.Size
### TLS is not mandatory
#V2: AND (UGT optHdr.NumberOfRvaAndSizes 9) (NEq tlsDir.VirtualAddress 0)
### Condition for a valid TLS table
#V3(V2): AND (UGT tlsDirEnd tlsDir.VirtualAddress) ULE tlsDirEnd imageEnd term
### Avoid to generate TLS directory
G1: OR (ULE optHdr.NumberOfRvaAndSizes 9) (Eq tlsDir 0) term
### Relocations
#### They come into play only if the image needs to be relocated.
#### This means that the ImageBase is either 0 or in the range of other DLLs
V4: OR (Eq optHdr.ImageBase 0) (UGE optHdr.ImageBase 0x70000000)
P: relocDir <- optHdr.DataDirectory[40, 8] as _IMAGE_DATA_DIRECTORY
P: relocVA <- relocDir.VirtualAddress
P: relocSize <- relocDir.Size
#### LdrRelocateImageWithBias:32
# V5(V4): AND (AND NEq relocVA 0 NEq relocSize 0) ULT relocVA imageEnd
V5(V4): AND (UGE optHdr.NumberOfRvaAndSizes 6) AND (NEq relocVA 0) (NEq relocSize 0)
### If the image is relocated, but doesn't have the reloc table, check that it wasn't stripped away, in which case the image is invalid
#### LdrRelocateImageWithBias:55
V6(V4, !V5): Eq BITAND fileHdr.Characteristics 0x1 0 term
P: tmpSize <- relocSize
P(V5): loopStart <- relocVA
L1(V5): relocBlockAddr <- VLOOP(loopStart, nextBlockAddr, V99, 2)
P: relocBlock <- HEADER[relocBlockAddr, 8]
P: blockSize <- relocBlock[4, 4]
P: blockPage <- relocBlock[0, 4]
G6: ULT blockPage 2 term
P: firstEntryAddr <- ADD relocBlockAddr 8
P: nEntry <- SHR (SUB blockSize 8) 1
P: tmpSize <- SUB tmpSize blockSize
P: nextBlockAddr <- ADD relocBlockAddr blockSize
V99: Neq tmpSize 0
P: tmpEntry <- INT 0 4
V96: UGE nEntry 1
L2(V96): entryAddr <- VLOOP(firstEntryAddr, nextBAddr, V98, 2)
P: entry <- HEADER[entryAddr, 2]
P: tmpEntry <- ADD tmpEntry 1
P: nextBAddr <- ADD entryAddr 2
P: relocType <- SHR BITAND entry[1] 0xf0 4
P: relocAddr <- BITAND entry 0xfff
V7: AND ULE relocType 10 NEq relocType 8 term
V8: ULT ADD blockPage relocAddr imageEnd term
G13: ULT ADD blockPage relocAddr FILESIZE term
## RelocType 4 uses two entries instead of 1
V9: Eq relocType 4
P(V9): tmpEntry <- ADD tmpEntry 1
P(V9): nextBAddr <- ADD nextBAddr 2
V98: ULE tmpEntry nEntry
END L2
V97: EQ tmpEntry nEntry term
END L1
G4: EQ tmpSize 0 term
### LdrpCheckForSafeDiscImage
#### Implicit constraints due to dereferencing fields in the headers
#### This is GT and not UGT to prevent undeflow!!!!!!
V10: GT SUB optHdr.SizeOfHeaders 0x2c 0 term
V11: ULT ADD optHdr.SizeOfHeaders 0x13 FILESIZE term
### LdrpCheckForSecuROMImage
#### Other implicit constraints, like the one above
P: debugDir <- optHdr.DataDirectory[48, 8] as _IMAGE_DATA_DIRECTORY
P: debugVA <- debugDir.VirtualAddress
P: debugSize <- debugDir.Size
P: nDebugEntry <- UDIV debugSize 28
V12: AND ULT optHdr.SectionAlignment 0x1000 NEq debugSize 0
V13(V12): ULT ADD debugVA 0x1c FILESIZE term
G14: ULE nDebugEntry 5 term
L3(V12): debugEntry <- LOOP(HEADER, debugVA, 0x1c, nDebugEntry, 5) as _IMAGE_DEBUG_DIRECTORY
P: dbgEntrySize <- debugEntry.SizeOfData
P: dbgPtrData <- debugEntry.PointerToRawData
V15: ULT (ADD dbgEntrySize dbgPtrData) FILESIZE term
END L3
#### LdrpCheckForSecuROMImage also checks that the certificate entry lies within the file. We do not support it for generation (it would need to create a valida certificate (which is impossible ofc)
P: certDir <- optHdr.DataDirectory[32, 8] as _IMAGE_DATA_DIRECTORY
# P: certDirVA <- certDir.VirtualAddress
# P: certDirSize <- certDir.Size
G16: EQ certDir 0 term
### Apparently this in not terminal...
# V17: ULE (ADD certDirSize certDirVA) FILESIZE term
### LdrpSetProtection: invoked before relocating to set the pages RWX
#### For each section, if it's not writable, it changes its permission, making it writable
P: sectTableOff <- ADD HEADER.e_lfanew (ADD fileHdr.SizeOfOptionalHeader 24)
P: nSections <- fileHdr.NumberOfSections
L4(V4): section <- LOOP(HEADER, sectTableOff, 40, nSections, 5) AS _IMAGE_SECTION_HEADER
P: charact <- section.Characteristics
P: virtSize <- section.VirtualSize
P: sizeRawData <- section.SizeOfRawData
P: VA <- section.VirtualAddress
V18: EQ (BITAND charact 0x80000000) 0
V19(V18): ULT VA FILESIZE term
V20(V18): ULT (ADD VA sizeRawData) FILESIZE term
END L4