Contains microcode uploading, proving and relocating functionality.
Marcel Sondaar
Educational Purposes
| ucode.asm | Contains microcode uploading, proving and relocating functionality. |
| Functions | |
| VerifyMicrocode | Attempts to proof that the microcode conforms to all invariants of the system. |
Attempts to proof that the microcode conforms to all invariants of the system.
To achieve this, the microcode is disassembled and each instruction is checked against the following security conditions
| Isolation | the microcode uses a fixed amount of global and local storage |
| Register invariant | Ensures that the value of important registers hold valid values (xSP, segments, etc) |
| I/O security | Ensures that only owned ports and memory areas are accessed |
| Termination | Verifies that the microcode terminates within reasonable time. Potentially valid uploads can be refused based on this constraint, since program flow instructions are required to be forward (conditional) jumps |
| Compatibility | Verifies that the microcode does not perform privileged or unsupported instructions |
The algorithm should allow for high-level functions to pass validity to minimize the need of assembly.
| ESI | the location of the microcode |
| EDI | the virutal address where storage is referenced |
| EDX | the size of local storage space |
| EBX | the size of the microcode |
| CF | set if validity could not be established |
| ESI | location of the instruction failing verification (valid when CF is set) |
| EAX | an error code relevant to the invariant (valid when CF is set) |
| EAX | the registers that were clobbered (valid when CF is clear) |
| +0..+3f | min/max values for GPRs |
| +40..+43 | ESP difference |
| +44..+47 | register usage |
| +48..+4B | maximum code address |