Modifying the Address Space

This chapter will focus on using the seL4 virtual address space (VSpace) APIs to manipulate the root task's own address space. Start by navigating to and running this chapter's example, which, so far, is empty.

cd workspaces/root-task/address-space
make simulate

In seL4, each thread is associated with a virtual address space (VSpace). A VSpace is comprised of a tree of translation tables mapping virtual addresses into physical frames of memory. VSpaces are represented by their root translation structures. While the high-level virtual address space API concepts are architecture-independent, the specific kernel object types for a given architecture mirror that architecture's paging structures. That said, all architectures share two object types:

• The top-level paging structure, called a VSpace, which is used to represent a virtual address space. In the sel4 crate, the corresponding sel4::CapType is sel4::cap_type::VSpace (note that, for some architectures, this is a type alias).
• Frames of physical memory. The set of possible frames sizes is architecture-dependant. See seL4 Reference Manual § 7.1.3 (Page). In the sel4 crate, sel4::cap_type::Granule is an alias for the sel4::CapType corresponding to the smallest frame object type.

The root task is provided with capabilites for the objects comprising its own virtual address space. The locations of these capabilities in the root task's CSpace is provided in the BootInfo struct. Our goal for this chapter will be to create a frame object and experiment with mapping it into the root task's own address space.

Step 4.A (exercise)       

Exercise: Using code snippets from Chapter 3 (Allocating Kernel Objects), create a frame object. We seek a value frame: sel4::cap::Granule (which can also be written as frame: sel4::Cap<sel4::cap_type::Granule>).

Note that, after importing the sel4::CapTypeForObjectOfFixedSize trait, you can express the appropriate sel4::ObjectBlueprint as sel4::cap_type::Granule::object_blueprint().

Step 4.B       

In order to avoid interacting with intermediate translation structures, let's reserve an aligned granule-sized region in the root task's program image that we can use for our experiment:

workspaces/root-task/address-space/src/main.rs:15:20 after 4.B

const GRANULE_SIZE: usize = sel4::FrameObjectType::GRANULE.bytes(); // 4096

#[repr(C, align(4096))]
struct PagePlaceholder(#[allow(dead_code)] [u8; GRANULE_SIZE]);

static mut PAGE_A: PagePlaceholder = PagePlaceholder([0xee; GRANULE_SIZE]);

workspaces/root-task/address-space/src/main.rs:46:49 after 4.B

    let page_a_addr = ptr::addr_of!(PAGE_A).cast::<u8>();
    sel4::debug_println!("PAGE_A: {page_a_addr:#x?}");
    assert_eq!(page_a_addr as usize % GRANULE_SIZE, 0);
    assert_eq!(unsafe { page_a_addr.read() }, 0xee);

This reservation covers exactly one page in the root task's virtual address space.

Step 4.C       

Let's unmap the page in the root task image that initially backs our reserved region. This will give us a hole in the root task VSpace, which we can use for our experiment.

This function determines the slot in the root task's CSpace of the page capability corresponding to the page in the root task's VSpace which contains the given address:

workspaces/root-task/address-space/src/main.rs:73:84 after 4.C

fn get_user_image_frame_slot(
    bootinfo: &sel4::BootInfo,
    addr: usize,
) -> sel4::init_thread::Slot<sel4::cap_type::Granule> {
    extern "C" {
        static __executable_start: usize;
    }
    let user_image_addr = ptr::addr_of!(__executable_start) as usize;
    bootinfo
        .user_image_frames()
        .index(addr / GRANULE_SIZE - user_image_addr / GRANULE_SIZE)
}

__executable_start is defined by the linker. We can use it, along with addr, to identify the offset into bootinfo.user_image_frames() of the capability we are after.

Use the get_user_image_frame_slot() function to find the capability corresponding to the frame backing our reserved region, and unmap that frame, leaving a hole in the root task's virtual address space. Try to access that region, and observe a page fault:

workspaces/root-task/address-space/src/main.rs:51:54 after 4.C

    let page_a_slot = get_user_image_frame_slot(bootinfo, page_a_addr as usize);
    page_a_slot.cap().frame_unmap().unwrap();

    unsafe { page_a_addr.read() };

Step 4.D (exercise)       

Exercise: Map new_frame at page_a_addr using new_frame.frame_map(), which corresponds to seL4_ARM_Page_Map.

Here are some hints for the parameters of .frame_map():

• vspace: A capability for the root task's VSpace can be expressed using sel4::init_thread::slot::VSPACE.cap().
• rights: sel4::CapRights::read_write() are the most permissive rights, and will work for our purposes.
• attrs: sel4::VmAttributes::default() will work here.