"""Independent, read-only verification of the C# GPT/FAT32 image writer."""
import hashlib
import json
import pathlib
import struct
import zlib
def inspect_image(path):
raw = pathlib.Path(path).read_bytes()
assert len(raw) % 512 == 0
last = len(raw) // 512 - 1
assert raw[510:512] == b'\x55\xaa' and raw[450] == 0xee
headers = []
for current, alternate, entries in [(1, last, 2), (last, 1, last - 32)]:
header = bytearray(raw[current * 512:(current + 1) * 512])
assert header[:8] == b'EFI PART'
assert struct.unpack_from('<II', header, 8) == (0x10000, 92)
expected_crc, = struct.unpack_from('<I', header, 16)
struct.pack_into('<I', header, 16, 0)
assert zlib.crc32(header[:92]) == expected_crc
assert struct.unpack_from('<QQQQ', header, 24) == (current, alternate, 34, last - 33)
assert struct.unpack_from('<QII', header, 72) == (entries, 128, 128)
table = raw[entries * 512:entries * 512 + 16384]
assert zlib.crc32(table) == struct.unpack_from('<I', header, 88)[0]
headers.append(table)
assert headers[0] == headers[1]
entry = headers[0][:128]
assert entry[:16] == bytes.fromhex('28732ac11ff8d211ba4b00a0c93ec93b')
first, end = struct.unpack_from('<QQ', entry, 32)
assert 34 <= first <= end <= last - 33
start = first * 512
bpb = raw[start:start + 512]
assert bpb[82:90] == b'FAT32 '
assert bpb[510:512] == b'\x55\xaa'
assert struct.unpack_from('<H', bpb, 11)[0] == 512
cluster_sectors = bpb[13]
assert cluster_sectors and not cluster_sectors & (cluster_sectors - 1)
reserved, = struct.unpack_from('<H', bpb, 14)
fats = bpb[16]
sectors, fat_sectors = struct.unpack_from('<II', bpb, 32)
assert sectors == end - first + 1 and fats == 2
assert raw[start + 6 * 512:start + 7 * 512] == bpb
info = raw[start + 512:start + 1024]
assert struct.unpack_from('<I', info, 0)[0] == 0x41615252
assert struct.unpack_from('<I', info, 484)[0] == 0x61417272
assert struct.unpack_from('<I', info, 508)[0] == 0xaa550000
assert raw[start + 7 * 512:start + 8 * 512] == info
fat_start = start + reserved * 512
fat_size = fat_sectors * 512
fat = raw[fat_start:fat_start + fat_size]
assert fat == raw[fat_start + fat_size:fat_start + fat_size * 2]
data_start = fat_start + fat_size * 2
cluster_bytes = cluster_sectors * 512
clusters = (sectors - reserved - fat_sectors * 2) // cluster_sectors
assert clusters >= 65525 and (clusters + 2) * 4 <= fat_size
root, = struct.unpack_from('<I', bpb, 44)
def chain(cluster, contiguous=False):
seen = set()
result = bytearray()
while cluster < 0x0ffffff8:
assert 2 <= cluster < clusters + 2 and cluster not in seen
seen.add(cluster)
offset = data_start + (cluster - 2) * cluster_bytes
assert start <= offset < offset + cluster_bytes <= (end + 1) * 512
result.extend(raw[offset:offset + cluster_bytes])
next_cluster = struct.unpack_from('<I', fat, cluster * 4)[0] & 0x0fffffff
if contiguous and next_cluster < 0x0ffffff8: assert next_cluster == cluster + 1, 'Workspace FAT allocation is no longer contiguous'
cluster = next_cluster
return bytes(result)
def entries(cluster):
values = chain(cluster)
long_names, long_sum = {}, None
for offset in range(0, len(values), 32):
value = values[offset:offset + 32]
if not value[0]: return
if value[0] == 0xe5: long_names = {}; continue
if value[11] == 0x0f:
index = value[0] & 31
assert index > 0
if value[0] & 64: long_names = {}; long_sum = value[13]
assert value[13] == long_sum
long_names[index] = value[1:11] + value[14:26] + value[28:32]
continue
if value[11] & 8: long_names = {}; continue
if long_names:
checksum = 0
for character in value[:11]:
checksum = (((checksum & 1) << 7) + (checksum >> 1) + character) & 255
assert checksum == long_sum
assert set(long_names) == set(range(1, max(long_names) + 1))
name = b''.join(long_names[index] for index in sorted(long_names)).decode('utf-16-le').split('\0')[0].rstrip('\uffff')
else:
name = value[:8].decode('ascii').rstrip()
extension = value[8:11].decode('ascii').rstrip()
if extension: name += '.' + extension
long_names = {}
child = struct.unpack_from('<H', value, 20)[0] << 16 | struct.unpack_from('<H', value, 26)[0]
yield name, value[11], child, struct.unpack_from('<I', value, 28)[0]
file_lbas = {}
def read_file(name):
cluster = root
components = name.split('/')
for index, component in enumerate(components):
matches = [entry for entry in entries(cluster) if entry[0].casefold() == component.casefold()]
assert len(matches) == 1, name
assert matches[0][0] == component, (name, matches[0][0])
_, attributes, cluster, size = matches[0]
if index < len(components) - 1: assert attributes & 16
else:
assert not attributes & 16
file_lbas[name] = (data_start + (cluster - 2) * cluster_bytes) // 512
value = chain(cluster, contiguous=name == 'Workspace.bin')
assert size <= len(value)
return value[:size]
file_paths, directories = [], set()
def walk(cluster, prefix='', depth=0):
assert depth < 8 and cluster not in directories, 'Cyclic or excessively nested FAT directory'
directories.add(cluster)
for name, attributes, child, _ in entries(cluster):
if name in ('.', '..'): continue
path = prefix + name
if attributes & 16: walk(child, path + '/', depth + 1)
else: file_paths.append(path)
assert len(file_paths) <= 1024, 'Unexpected FAT file count'
walk(root)
files = {name: read_file(name) for name in ['EFI/BOOT/BOOTX64.EFI', 'EFI/XFE/Limine.efi', 'System/Kernel.elf', 'System/BootShim.json', 'Limine.conf']}
if 'boot():/System/Console.elf' in files['Limine.conf'].decode('utf-8'):
files['System/Console.elf'] = read_file('System/Console.elf')
if 'Workspace.bin' in file_paths:
files['Workspace.bin'] = read_file('Workspace.bin')
files['UserFiles/UsbHello.dll'] = read_file('UserFiles/UsbHello.dll')
metadata = json.loads(files['System/BootShim.json'])
assert metadata['Kind'] == 'XfeEfiDisplayInitializer'
assert metadata['BootPath'] == 'EFI/BOOT/BOOTX64.EFI'
assert metadata['ChainloadPath'] == 'EFI/XFE/Limine.efi'
assert metadata['ArtifactSha256'] == hashlib.sha256(files['EFI/BOOT/BOOTX64.EFI']).hexdigest()
assert metadata['KernelLanguage'] == 'C# NativeAOT' and metadata['HelperLanguage'] == 'C# UEFI'
assert 'Source/XFESystem.Boot/EfiEntry.cs' in metadata['SourceSha256'] and 'Source/XFESystem.Boot/DisplayContracts.cs' in metadata['SourceSha256']
return {'ImageSha256': hashlib.sha256(raw).hexdigest(),
'GptPrimaryAndBackupVerified': True, 'FatMirrorsVerified': True,
'FatBootAndFsInfoBackupsVerified': True,
'DisplayInitializerMetadataVerified': True, 'BootShimSourceSha256': metadata['SourceSha256'],
'FilePaths': sorted(file_paths),
'FileFirstLbas': file_lbas,
'Files': {name: hashlib.sha256(content).hexdigest() for name, content in files.items()}}, files
def verify_single_edition(inspection, files, manifest):
"""Check the actual FAT inventory and boot configuration, not just a filename or label."""
edition = manifest.get('Edition')
assert edition in ('Console', 'Desktop'), 'Select one Console or Desktop system'
assert manifest.get('DeploymentPolicy') == 'SingleEditionOnly', 'Single-system deployment policy is required'
usb = manifest.get('UsbWorkspace') is True
assert manifest.get('ImageBytes') == (256 if usb else 128) * 1024 * 1024, 'Unexpected single-system image size'
assert manifest.get('BootEntries') == [edition] and manifest.get('DefaultBootEntry') == edition, 'Exactly one boot entry is required'
assert manifest.get('BootMenuTimeoutSeconds') == 0, 'A single-system image must enter without a selection menu'
assert not any(manifest.get(name) for name in ('ConsoleKernelPath', 'ConsoleKernelSha256', 'IndependentConsoleKernelBuild')), 'A second kernel is not permitted'
expected_paths = sorted(['EFI/BOOT/BOOTX64.EFI', 'EFI/XFE/Limine.efi', 'System/Kernel.elf', 'System/BootShim.json', 'Limine.conf'])
if usb:
expected_paths = sorted(expected_paths + ['Workspace.bin','UserFiles/UsbHello.dll'])
descriptor = files['Workspace.bin'][:512]
assert len(files['Workspace.bin']) == manifest.get('WorkspaceBytes') == 64 * 1024 * 1024
assert struct.unpack_from('<QIII',descriptor) == (0x5357425355454658,1,131072,65535)
assert struct.unpack_from('<I',descriptor,20)[0] == zlib.crc32(descriptor[:20])
assert manifest.get('WorkspaceFirstLba') == inspection['FileFirstLbas']['Workspace.bin']
assert inspection.get('FilePaths') == expected_paths, 'Unexpected files or additional system kernels in the actual FAT image'
expected_config = ('timeout: 0\nserial: yes\nverbose: no\nterse: yes\nquiet: yes\nfirmware_logo: no\n\n'
f'/XFESystem {edition}\n protocol: limine\n resolution: {manifest["Resolution"]}x32\n path: boot():/System/Kernel.elf\n')
assert files['Limine.conf'].decode('utf-8') == expected_config, 'The actual boot configuration must silently start only the selected system'
assert manifest.get('IndependentKernelBuild', {}).get('Edition') == edition, 'The selected kernel edition differs'
return {'Kind': 'XfeSingleEditionImageProof', 'Passed': True, 'Edition': edition,
'KernelCount': 1, 'BootEntryCount': 1, 'SystemSelectionMenu': False, 'BootMenuTimeoutSeconds': 0,
'UsbWorkspace': usb,
'FilePaths': expected_paths, 'ConfigurationSha256': hashlib.sha256(files['Limine.conf']).hexdigest()}
"""Independent, read-only verification of the C# GPT/FAT32 image writer."""
import hashlib
import json
import pathlib
import struct
import zlib
def inspect_image(path):
raw = pathlib.Path(path).read_bytes()
assert len(raw) % 512 == 0
last = len(raw) // 512 - 1
assert raw[510:512] == b'\x55\xaa' and raw[450] == 0xee
headers = []
for current, alternate, entries in [(1, last, 2), (last, 1, last - 32)]:
header = bytearray(raw[current * 512:(current + 1) * 512])
assert header[:8] == b'EFI PART'
assert struct.unpack_from('<II', header, 8) == (0x10000, 92)
expected_crc, = struct.unpack_from('<I', header, 16)
struct.pack_into('<I', header, 16, 0)
assert zlib.crc32(header[:92]) == expected_crc
assert struct.unpack_from('<QQQQ', header, 24) == (current, alternate, 34, last - 33)
assert struct.unpack_from('<QII', header, 72) == (entries, 128, 128)
table = raw[entries * 512:entries * 512 + 16384]
assert zlib.crc32(table) == struct.unpack_from('<I', header, 88)[0]
headers.append(table)
assert headers[0] == headers[1]
entry = headers[0][:128]
assert entry[:16] == bytes.fromhex('28732ac11ff8d211ba4b00a0c93ec93b')
first, end = struct.unpack_from('<QQ', entry, 32)
assert 34 <= first <= end <= last - 33
start = first * 512
bpb = raw[start:start + 512]
assert bpb[82:90] == b'FAT32 '
assert bpb[510:512] == b'\x55\xaa'
assert struct.unpack_from('<H', bpb, 11)[0] == 512
cluster_sectors = bpb[13]
assert cluster_sectors and not cluster_sectors & (cluster_sectors - 1)
reserved, = struct.unpack_from('<H', bpb, 14)
fats = bpb[16]
sectors, fat_sectors = struct.unpack_from('<II', bpb, 32)
assert sectors == end - first + 1 and fats == 2
assert raw[start + 6 * 512:start + 7 * 512] == bpb
info = raw[start + 512:start + 1024]
assert struct.unpack_from('<I', info, 0)[0] == 0x41615252
assert struct.unpack_from('<I', info, 484)[0] == 0x61417272
assert struct.unpack_from('<I', info, 508)[0] == 0xaa550000
assert raw[start + 7 * 512:start + 8 * 512] == info
fat_start = start + reserved * 512
fat_size = fat_sectors * 512
fat = raw[fat_start:fat_start + fat_size]
assert fat == raw[fat_start + fat_size:fat_start + fat_size * 2]
data_start = fat_start + fat_size * 2
cluster_bytes = cluster_sectors * 512
clusters = (sectors - reserved - fat_sectors * 2) // cluster_sectors
assert clusters >= 65525 and (clusters + 2) * 4 <= fat_size
root, = struct.unpack_from('<I', bpb, 44)
def chain(cluster, contiguous=False):
seen = set()
result = bytearray()
while cluster < 0x0ffffff8:
assert 2 <= cluster < clusters + 2 and cluster not in seen
seen.add(cluster)
offset = data_start + (cluster - 2) * cluster_bytes
assert start <= offset < offset + cluster_bytes <= (end + 1) * 512
result.extend(raw[offset:offset + cluster_bytes])
next_cluster = struct.unpack_from('<I', fat, cluster * 4)[0] & 0x0fffffff
if contiguous and next_cluster < 0x0ffffff8: assert next_cluster == cluster + 1, 'Workspace FAT allocation is no longer contiguous'
cluster = next_cluster
return bytes(result)
def entries(cluster):
values = chain(cluster)
long_names, long_sum = {}, None
for offset in range(0, len(values), 32):
value = values[offset:offset + 32]
if not value[0]: return
if value[0] == 0xe5: long_names = {}; continue
if value[11] == 0x0f:
index = value[0] & 31
assert index > 0
if value[0] & 64: long_names = {}; long_sum = value[13]
assert value[13] == long_sum
long_names[index] = value[1:11] + value[14:26] + value[28:32]
continue
if value[11] & 8: long_names = {}; continue
if long_names:
checksum = 0
for character in value[:11]:
checksum = (((checksum & 1) << 7) + (checksum >> 1) + character) & 255
assert checksum == long_sum
assert set(long_names) == set(range(1, max(long_names) + 1))
name = b''.join(long_names[index] for index in sorted(long_names)).decode('utf-16-le').split('\0')[0].rstrip('\uffff')
else:
name = value[:8].decode('ascii').rstrip()
extension = value[8:11].decode('ascii').rstrip()
if extension: name += '.' + extension
long_names = {}
child = struct.unpack_from('<H', value, 20)[0] << 16 | struct.unpack_from('<H', value, 26)[0]
yield name, value[11], child, struct.unpack_from('<I', value, 28)[0]
file_lbas = {}
def read_file(name):
cluster = root
components = name.split('/')
for index, component in enumerate(components):
matches = [entry for entry in entries(cluster) if entry[0].casefold() == component.casefold()]
assert len(matches) == 1, name
assert matches[0][0] == component, (name, matches[0][0])
_, attributes, cluster, size = matches[0]
if index < len(components) - 1: assert attributes & 16
else:
assert not attributes & 16
file_lbas[name] = (data_start + (cluster - 2) * cluster_bytes) // 512
value = chain(cluster, contiguous=name == 'Workspace.bin')
assert size <= len(value)
return value[:size]
file_paths, directories = [], set()
def walk(cluster, prefix='', depth=0):
assert depth < 8 and cluster not in directories, 'Cyclic or excessively nested FAT directory'
directories.add(cluster)
for name, attributes, child, _ in entries(cluster):
if name in ('.', '..'): continue
path = prefix + name
if attributes & 16: walk(child, path + '/', depth + 1)
else: file_paths.append(path)
assert len(file_paths) <= 1024, 'Unexpected FAT file count'
walk(root)
files = {name: read_file(name) for name in ['EFI/BOOT/BOOTX64.EFI', 'EFI/XFE/Limine.efi', 'System/Kernel.elf', 'System/BootShim.json', 'Limine.conf']}
if 'boot():/System/Console.elf' in files['Limine.conf'].decode('utf-8'):
files['System/Console.elf'] = read_file('System/Console.elf')
if 'Workspace.bin' in file_paths:
files['Workspace.bin'] = read_file('Workspace.bin')
files['UserFiles/UsbHello.dll'] = read_file('UserFiles/UsbHello.dll')
metadata = json.loads(files['System/BootShim.json'])
assert metadata['Kind'] == 'XfeEfiDisplayInitializer'
assert metadata['BootPath'] == 'EFI/BOOT/BOOTX64.EFI'
assert metadata['ChainloadPath'] == 'EFI/XFE/Limine.efi'
assert metadata['ArtifactSha256'] == hashlib.sha256(files['EFI/BOOT/BOOTX64.EFI']).hexdigest()
assert metadata['KernelLanguage'] == 'C# NativeAOT' and metadata['HelperLanguage'] == 'C# UEFI'
assert 'Source/XFESystem.Boot/EfiEntry.cs' in metadata['SourceSha256'] and 'Source/XFESystem.Boot/DisplayContracts.cs' in metadata['SourceSha256']
return {'ImageSha256': hashlib.sha256(raw).hexdigest(),
'GptPrimaryAndBackupVerified': True, 'FatMirrorsVerified': True,
'FatBootAndFsInfoBackupsVerified': True,
'DisplayInitializerMetadataVerified': True, 'BootShimSourceSha256': metadata['SourceSha256'],
'FilePaths': sorted(file_paths),
'FileFirstLbas': file_lbas,
'Files': {name: hashlib.sha256(content).hexdigest() for name, content in files.items()}}, files
def verify_single_edition(inspection, files, manifest):
"""Check the actual FAT inventory and boot configuration, not just a filename or label."""
edition = manifest.get('Edition')
assert edition in ('Console', 'Desktop'), 'Select one Console or Desktop system'
assert manifest.get('DeploymentPolicy') == 'SingleEditionOnly', 'Single-system deployment policy is required'
usb = manifest.get('UsbWorkspace') is True
assert manifest.get('ImageBytes') == (256 if usb else 128) * 1024 * 1024, 'Unexpected single-system image size'
assert manifest.get('BootEntries') == [edition] and manifest.get('DefaultBootEntry') == edition, 'Exactly one boot entry is required'
assert manifest.get('BootMenuTimeoutSeconds') == 0, 'A single-system image must enter without a selection menu'
assert not any(manifest.get(name) for name in ('ConsoleKernelPath', 'ConsoleKernelSha256', 'IndependentConsoleKernelBuild')), 'A second kernel is not permitted'
expected_paths = sorted(['EFI/BOOT/BOOTX64.EFI', 'EFI/XFE/Limine.efi', 'System/Kernel.elf', 'System/BootShim.json', 'Limine.conf'])
if usb:
expected_paths = sorted(expected_paths + ['Workspace.bin','UserFiles/UsbHello.dll'])
descriptor = files['Workspace.bin'][:512]
assert len(files['Workspace.bin']) == manifest.get('WorkspaceBytes') == 64 * 1024 * 1024
assert struct.unpack_from('<QIII',descriptor) == (0x5357425355454658,1,131072,65535)
assert struct.unpack_from('<I',descriptor,20)[0] == zlib.crc32(descriptor[:20])
assert manifest.get('WorkspaceFirstLba') == inspection['FileFirstLbas']['Workspace.bin']
assert inspection.get('FilePaths') == expected_paths, 'Unexpected files or additional system kernels in the actual FAT image'
expected_config = ('timeout: 0\nserial: yes\nverbose: no\nterse: yes\nquiet: yes\nfirmware_logo: no\n\n'
f'/XFESystem {edition}\n protocol: limine\n resolution: {manifest["Resolution"]}x32\n path: boot():/System/Kernel.elf\n')
assert files['Limine.conf'].decode('utf-8') == expected_config, 'The actual boot configuration must silently start only the selected system'
assert manifest.get('IndependentKernelBuild', {}).get('Edition') == edition, 'The selected kernel edition differs'
return {'Kind': 'XfeSingleEditionImageProof', 'Passed': True, 'Edition': edition,
'KernelCount': 1, 'BootEntryCount': 1, 'SystemSelectionMenu': False, 'BootMenuTimeoutSeconds': 0,
'UsbWorkspace': usb,
'FilePaths': expected_paths, 'ConfigurationSha256': hashlib.sha256(files['Limine.conf']).hexdigest()}