seL4_libs icon indicating copy to clipboard operation
seL4_libs copied to clipboard

libsel4vka: Fix size bits in vka_untyped_retype for seL4_CapTableObject

Open astevins opened this issue 7 months ago • 3 comments

The size bits for a untyped retype to seL4_CapTableObject are calculated incorrectly when using vka_untyped_retype

  • seL4_SlotBits is added once in vka: https://github.com/seL4/seL4_libs/blob/fcabdef37016cd568a40c82e0d97a264b86ee6d4/libsel4vka/include/vka/capops.h#L130
  • And it is added again during the syscall: https://github.com/seL4/seL4/blob/c679fe77d6441cd412dd253d953ee833dd25d740/src/object/untyped.c#L75

The result is that seL4_SlotBits is added twice, causing the UntypedRetype operation to fail with "Insufficient memory" for this simple test:

int test_retype_cap_table_object(env_t env)
{
    int error;
    size_t cspace_size_bits = 17;

    vka_object_t untyped;
    error = vka_alloc_untyped(&env->vka, cspace_size_bits + seL4_SlotBits, &untyped);
    test_error_eq(error, 0);

    cspacepath_t cnode_dest;
    error = vka_cspace_alloc_path(&env->vka, &cnode_dest);
    test_error_eq(error, 0);

    error = vka_untyped_retype(&untyped, seL4_CapTableObject, cspace_size_bits, 1, &cnode_dest);
    test_error_eq(error, 0);
}

A simple solution is to subtract seL4_SlotBits before calling seL4_Untyped_Retype.

astevins avatar Jul 22 '24 18:07 astevins