-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLdrpInitializeProcess.lmod
192 lines (162 loc) · 7.62 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
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
LOADREL ntkrnlmp
DEFINE FILESIZE 500
INPUT HEADER FILESIZE as DOSHeader
P: zero <- INT 0 4
P: one <- INT 1 4
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: nSections <- fileHdr.NumberOfSections
P: sectionTableOffset <- ADD HEADER.e_lfanew (ADD fileHdr.SizeOfOptionalHeader 24)
P: imageEnd <- ADD optHdr.ImageBase optHdr.SizeOfImage
G999: NOT OVFLADD optHdr.ImageBase optHdr.SizeOfImage term
#### LdrpValidateEntrySection
V1: OR (Eq optHdr.AddressOfEntryPoint 0) (UGE optHdr.AddressOfEntryPoint optHdr.SizeOfHeaders) term
## Needs relocation?
# V2: UGE optHdr.ImageBase 0x80000000
V2: OR (EQ optHdr.ImageBase 0) (UGE optHdr.ImageBase 0x80000000)
G1: ULE nSections 5 term
G99: NEq nSections 0 term
P: defaultNewBase <- INT 0x10000 4
L1(V2): section <- LOOP(HEADER, sectionTableOffset, 40, nSections, 5) AS _IMAGE_SECTION_HEADER
P: size <- section.SizeOfRawData
P: VA <- section.VirtualAddress
P: endSect <- ADD VA (ALIGNUP size optHdr.SectionAlignment)
P: charact <- section.Characteristics
V3: OR (AND (UGT endSect imageEnd) (NEq size 0)) (UGT ADD defaultNewBase VA 0x80000000)
V4(V3): EQ (BITAND charact[3] 0x80) 0x80 term
END L1
### 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
P: relocDir <- optHdr.DataDirectory[40, 8] as _IMAGE_DATA_DIRECTORY
P: relocVA <- relocDir.VirtualAddress
P: relocSize <- relocDir.Size
#### LdrRelocateImageWithBias:45,48
V6(V2): AND (UGE optHdr.NumberOfRvaAndSizes 6) AND (NEq relocVA 0) (NEq relocSize 0)
#V6(V2): AND (UGE optHdr.NumberOfRvaAndSizes 5) AND (NEq relocVA 0) (NEq relocSize 0) term
G7(V6): ULT relocSize 0x100 term
### 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:46,49
V7(V2, !V6): EQ BITAND fileHdr.Characteristics 1 0 term
P: tmpSize <- relocSize
P(V6): loopStart <- relocVA
L2(V6): 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
L3(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
## LdrRelocateImageWithBias:47
### Checks that the RtlImageNtHeader is still valid
### Meaning that the targeted addre can't be 0x0 or 0x1...
V15: OR (EQ relocType 0) AND (NEQ relocAddr 0) (NEQ relocAddr 1) term
### Can't overlap with e_lfanew (0x3f-0x40)
V16: OR (EQ relocType 0) OR (ULT relocAddr 0x3f) (UGT relocAddr 0x40) term
### Cant' overlap with PE magic (e_lfanew-e_lfanew+4)
V17: OR (EQ relocType 0) OR (ULT relocAddr HEADER.e_lfanew) (UGT relocAddr ADD HEADER.e_lfanew 4) term
V11: EQ (BITAND (SHL one (SHR entry 12)) 0x3a0) 0 term
V12: OR EQ relocType 10 ULE relocType 4 term
V13: ULT ADD blockPage relocAddr imageEnd term
G13: ULT ADD blockPage relocAddr FILESIZE term
## RelocType 4 uses two entries instead of 1
V14: Eq relocType 4
P(V14): tmpEntry <- ADD tmpEntry 1
P(V14): nextBAddr <- ADD nextBAddr 2
V98: ULT tmpEntry nEntry
END L3
V97: EQ tmpEntry nEntry term
END L2
G95: EQ tmpSize 0 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
V151: AND ULT optHdr.SectionAlignment 0x1000 NEq debugSize 0
G2(V151): AND (ULT optHdr.SectionAlignment 0x1000) (ULE nDebugEntry 5) term
L4(V151): debugEntry <- LOOP(HEADER, debugVA, 0x1c, nDebugEntry, 5) as _IMAGE_DEBUG_DIRECTORY
P: dbgEntrySize <- debugEntry.SizeOfData
P: dbgPtrData <- debugEntry.PointerToRawData
V16: ULT (ADD dbgEntrySize dbgPtrData) FILESIZE term
END L4
#### 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
G3: EQ certDir 0 term
V17: ULE (ADD certDirSize certDirVA) FILESIZE term
### LdrpCheckForSafeDiscImage
#### Implicit constraints due to dereferencing fields in the headers
#### GT, not UGT
V18: GT SUB optHdr.SizeOfHeaders 0x2c 0 term
V19: ULT ADD optHdr.SizeOfHeaders 0x13 FILESIZE term
### LdrpInitializeTls
#### If the directory is defined it must lay inside the image
P: tlsDir <- optHdr.DataDirectory[72, 8] as _IMAGE_DATA_DIRECTORY
P: tlsDirEnd <- ADD tlsDir.VirtualAddress tlsDir.Size
V20: AND (UGT optHdr.NumberOfRvaAndSizes 9) (NEq tlsDir.VirtualAddress 0)
V21(V20): UGT (SUB 0xffffffff tlsDir.VirtualAddress) tlsDir.Size term
V22(V20): ULE tlsDirEnd imageEnd term
G5: OR (ULE optHdr.NumberOfRvaAndSizes 9) (Eq tlsDir 0) term
### LdrpGetImportDescriptorForSnap
#### If the import directory has VA (no matter the number of RVAs) the size can't be 0
P: importDir <- optHdr.DataDirectory[8, 8] as _IMAGE_DATA_DIRECTORY
V23: OR (NEq importDir.Size 0) (EQ importDir.VirtualAddress 0) term
G8: EQ importDir 0 term
### LdrpProcessMappedModule
P: ldDir <- optHdr.DataDirectory[80, 16] as _IMAGE_DATA_DIRECTORY
P: ldVA <- ldDir.VirtualAddress
P: ldSize <- ldDir.Size
P: majSub <- optHdr.MajorSubsystemVersion
P: minSub <- optHdr.MinorSubsystemVersion
V24: OR (UGE majSub 7) (AND (EQ majSub 6) (UGE minSub 3))
V25(V24): AND (ULT (ADD ldVA 120) imageEnd) (NOT OVFLADD ldVA 120) term
V26(V24): AND (GT optHdr.NumberOfRvaAndSizes 10) (UGE ldSize 0x40) term
V27(V24): UGE optHdr.SectionAlignment 0x1000
P: ldOff <- INT 0 4
P(V24, !V27): ldOff <- ldVA
P: found <- INT 0 1
L5(V27): section <- LOOP(HEADER, sectionTableOffset, 40, nSections, 5) AS _IMAGE_SECTION_HEADER
P: RVA <- section.VirtualAddress
P: sizeRawData <- section.SizeOfRawData
P: VirtSize <- section.VirtualSize
P: size <- VirtSize
V28: ULT section.PointerToRawData 0x200
P: sectOff <- section.PointerToRawData
P(V28): sectOff <- ALIGNDOWN section.PointerToRawData optHdr.FileAlignment
G9: GT section.PointerToRawData 0 term
V29: EQ VirtSize 0
P(V29): size <- sizeRawData
P: sectEnd <- ADD RVA size
V30: AND (ULE RVA ldVA) (UGT sectEnd ldVA)
P(V30): found <- INT 1 1
P(V30): ldOff <- ADD sectOff (SUB ldVA RVA)
G10(V30): AND NEq ldOff 0 UGT sizeRawData 124 term
G11(V30): AND (NOT OVFLADD sectOff sizeRawData) (ULT ADD sectOff sizeRawData FILESIZE) term
END L5
V30(V27): EQ found 1 term
V31(V27): NEQ ldOff 0 term
P: cookieAddr <- HEADER[ADD ldOff 60, 4]
P: ldCharact <- HEADER[ldOff, 4]
V32(V24, !V2): AND (UGT cookieAddr optHdr.ImageBase) (ULT (ADD cookieAddr 4) imageEnd) term
G33(V24, V2): AND (UGT cookieAddr 0x10000) (ULT (ADD cookieAddr 4) (ADD optHdr.SizeOfImage 0x10000)) term
G14(V24): EQ cookieAddr ADD ldVA 120
P: cookieOff <- ADD ldOff 120
G15(V24): EQ HEADER[cookieOff, 4] 0xBB40E64E term
V35(V24): UGE ldCharact 0x48 term
P: exportDir <- optHdr.DataDirectory[0, 8]
G16: EQ exportDir 0 term