Blog

Transition to Ring 3 – User Space Isolation

August, 2026

One of the biggest milestones in Daxo OS was the successful move from Ring 0 to Ring 3. This involved setting up proper GDT entries for user code/data, configuring a TSS with a privilege‑stack table, and implementing the iretq jump.

The main pitfall was forgetting the USER_ACCESSIBLE flag on the page table entry – without it, any fetch from Ring 3 caused a page fault. Debugging with QEMU’s -d int and examining CR2 registers helped identify the issue.

Now the kernel can map isolated pages, write a simple infinite loop, and jump into it. The user program uses syscall to interact with the kernel.

Read more about the implementation →

ATA Driver Deep Dive: Polling vs Interrupts

July, 2026

The ATA driver uses PIO (Programmed I/O) to read sectors. Because interrupts are disabled during early boot, the driver polls the status registers. The tricky part was ensuring the drive is ready and that we don’t miss any data.

I implemented wait_ready and wait_data loops with timeouts. The driver is now stable and can read the test string from the first sector of disk.bin.

Check the driver details →

Formal Verification of the Frame Allocator

June, 2026

To increase confidence in the kernel’s memory management, I modelled the physical frame allocator in Lean 4. The allocator state is a list of frames, each with an address and a free flag.

The theorem allocate_marks_as_allocated states that after a successful allocation, the returned frame is marked as used. This proof ensures no double‑allocation or use‑after‑free at the specification level.

See the verification details →