From 2e343765caaff60a3b0fed1a8377e25588a5dae0 Mon Sep 17 00:00:00 2001 From: Ivan-Velickovic Date: Tue, 23 May 2023 13:35:28 +1000 Subject: [PATCH 1/4] More extensive testing of ARM caching operations Signed-off-by: Ivan-Velickovic --- apps/sel4test-tests/src/tests/cache.c | 226 ++++++++++++++++++++++++++ 1 file changed, 226 insertions(+) diff --git a/apps/sel4test-tests/src/tests/cache.c b/apps/sel4test-tests/src/tests/cache.c index d31d186c..4cc895d1 100644 --- a/apps/sel4test-tests/src/tests/cache.c +++ b/apps/sel4test-tests/src/tests/cache.c @@ -327,3 +327,229 @@ static int test_page_uncached_after_retype(env_t env) DEFINE_TEST(CACHEFLUSH0004, "Test that mapping a frame uncached doesn't see stale data after retype", test_page_uncached_after_retype, config_set(CONFIG_HAVE_CACHE)) + +#if defined(CONFIG_ARCH_ARM) + +/* + * The following tests aim to test the seL4_ARM_* cache operations on every + * kind of frame mapping that can be created. The motivation behind this is + * that some ARM hardware cache instructions generate faults depending on the + * permissions of the mapping and we need to ensure that the kernel catches + * these so that a fault does not occur in kernel space. In addition, these + * tests ensure that the kernel is enforcing a frame's cap rights, depending + * on the cache operation. + * + * For each kind of mapping we need to test the following operations: + * + * seL4_ARM_VSpace_Clean_Data + * seL4_ARM_VSpace_Invalidate_Data + * seL4_ARM_VSpace_CleanInvalidate_Data + * seL4_ARM_VSpace_Unify_Instruction + * seL4_ARM_Page_Clean_Data + * seL4_ARM_Page_Invalidate_Data + * seL4_ARM_Page_CleanInvalidate_Data + * seL4_ARM_Page_Unify_Instruction + * + */ +static int test_cache_invalid(env_t env) +{ + seL4_CPtr frame; + uintptr_t vstart; + int err; + void *vaddr; + reservation_t reservation; + vka_t *vka = &env->vka; + + reservation = vspace_reserve_range(&env->vspace, PAGE_SIZE_4K, seL4_AllRights, 1, &vaddr); + assert(reservation.res); + + vstart = (uintptr_t)vaddr; + assert(IS_ALIGNED(vstart, seL4_PageBits)); + + /* Create a frame, but deliberately do not create a mapping for it. */ + frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K); + test_assert(frame != seL4_CapNull); + + /* Top-level page table operations for invalid mappings are silently ignored by + * the kernel so we do not test them here */ + + /* Page-level operations */ + err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_FailedLookup); + err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_FailedLookup); + err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_FailedLookup); + err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_FailedLookup); + + return sel4test_get_result(); +} + +static int test_cache_kernel_only(env_t env) +{ + /* + * This test makes a mapping to a frame with seL4_NoRights, this means + * that the kernel will map it in with the kernel-only VM attribute. + */ + seL4_CPtr frame; + uintptr_t vstart; + vka_t *vka; + int err; + + vka = &env->vka; + + void *vaddr; + reservation_t reservation; + + reservation = vspace_reserve_range(&env->vspace, + PAGE_SIZE_4K, seL4_NoRights, 1, &vaddr); + assert(reservation.res); + + vstart = (uintptr_t)vaddr; + assert(IS_ALIGNED(vstart, seL4_PageBits)); + + /* Create a frame */ + frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K); + test_assert(frame != seL4_CapNull); + + /* map in a cap with cacheability */ + err = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation); + test_error_eq(err, seL4_NoError); + + /* Since the mapping is kernel-only, all of these invocations should fail.*/ + + /* Top-level page table operations */ + err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + /* Page-level operations */ + err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + + return sel4test_get_result(); +} + +static int test_cache_read_write(env_t env) +{ + seL4_CPtr frame; + uintptr_t vstart; + vka_t *vka; + int err; + + vka = &env->vka; + + void *vaddr; + reservation_t reservation; + + reservation = vspace_reserve_range(&env->vspace, + PAGE_SIZE_4K, seL4_AllRights, 1, &vaddr); + assert(reservation.res); + + vstart = (uintptr_t)vaddr; + assert(IS_ALIGNED(vstart, seL4_PageBits)); + + /* Create a frame */ + frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K); + test_assert(frame != seL4_CapNull); + + /* map in a cap with cacheability */ + err = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation); + test_error_eq(err, seL4_NoError); + + /* Now that we have setup the read-write mapping, we can test all the caching operations. */ + + /* Top-level page table operations */ + err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + /* Page-level operations */ + err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + + return sel4test_get_result(); +} + +static int test_cache_read_only(env_t env) +{ + seL4_CPtr frame; + uintptr_t vstart; + vka_t *vka; + int err; + + vka = &env->vka; + + void *vaddr; + reservation_t reservation; + + reservation = vspace_reserve_range(&env->vspace, + PAGE_SIZE_4K, seL4_CanRead, 1, &vaddr); + assert(reservation.res); + + vstart = (uintptr_t)vaddr; + assert(IS_ALIGNED(vstart, seL4_PageBits)); + + /* Create a frame */ + frame = vka_alloc_frame_leaky(vka, PAGE_BITS_4K); + test_assert(frame != seL4_CapNull); + + /* map in a cap with cacheability */ + err = vspace_map_pages_at_vaddr(&env->vspace, &frame, NULL, vaddr, 1, seL4_PageBits, reservation); + test_error_eq(err, seL4_NoError); + + /* Now that we have setup the read-only mapping, we can test all the caching operations. */ + + /* Top-level page table operations */ + err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + /* Page-level operations */ + err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + + return sel4test_get_result(); +} + +DEFINE_TEST(CACHEFLUSH0005, "Test cache maintenance on invalid mappings", test_cache_invalid, + config_set(CONFIG_HAVE_CACHE)) +DEFINE_TEST(CACHEFLUSH0006, "Test cache maintenance on kernel-only mappings", test_cache_kernel_only, + config_set(CONFIG_HAVE_CACHE)) +DEFINE_TEST(CACHEFLUSH0007, "Test cache maintenance on read-write mappings", test_cache_read_write, + config_set(CONFIG_HAVE_CACHE)) +DEFINE_TEST(CACHEFLUSH0008, "Test cache maintenance on read-only mappings", test_cache_read_only, + config_set(CONFIG_HAVE_CACHE)) + +#endif From 354898cda7ae4a4a366230b18f1d334a334b49a6 Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 18 Jun 2024 11:09:19 +1000 Subject: [PATCH 2/4] Fixes to get cache tests passing Signed-off-by: Ivan Velickovic --- apps/sel4test-tests/src/tests/cache.c | 53 ++++++++++++++------------- 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/apps/sel4test-tests/src/tests/cache.c b/apps/sel4test-tests/src/tests/cache.c index 4cc895d1..0290a997 100644 --- a/apps/sel4test-tests/src/tests/cache.c +++ b/apps/sel4test-tests/src/tests/cache.c @@ -374,14 +374,14 @@ static int test_cache_invalid(env_t env) * the kernel so we do not test them here */ /* Page-level operations */ - err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_FailedLookup); - err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_FailedLookup); - err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_FailedLookup); - err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_FailedLookup); + err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_CleanInvalidate_Data(frame, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_IllegalOperation); return sel4test_get_result(); } @@ -421,22 +421,23 @@ static int test_cache_kernel_only(env_t env) /* Top-level page table operations */ err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, seL4_NoError); err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_IllegalOperation); err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, seL4_NoError); err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, seL4_NoError); /* Page-level operations */ - err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); - err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); - err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); - err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); + printf("kernel_only: page clean err: 0x%lx\n", err); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_IllegalOperation); + err = seL4_ARM_Page_CleanInvalidate_Data(frame, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); + err = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K); + test_error_eq(err, seL4_NoError); return sel4test_get_result(); } @@ -480,13 +481,13 @@ static int test_cache_read_write(env_t env) err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); /* Page-level operations */ - err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); - err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); - err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_CleanInvalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); - err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); return sel4test_get_result(); @@ -531,13 +532,13 @@ static int test_cache_read_only(env_t env) err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); /* Page-level operations */ - err = seL4_ARM_Page_Clean_Data(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); - err = seL4_ARM_Page_Invalidate_Data(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_IllegalOperation); - err = seL4_ARM_Page_CleanInvalidate_Data(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_CleanInvalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); - err = seL4_ARM_Page_Unify_Instruction(vstart, 0, PAGE_SIZE_4K); + err = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); return sel4test_get_result(); From 36dd4cf63deb1d387c5433c8701aa5ad4c1b4fdd Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 18 Jun 2024 12:31:17 +1000 Subject: [PATCH 3/4] Remove debug print Signed-off-by: Ivan Velickovic --- apps/sel4test-tests/src/tests/cache.c | 1 - 1 file changed, 1 deletion(-) diff --git a/apps/sel4test-tests/src/tests/cache.c b/apps/sel4test-tests/src/tests/cache.c index 0290a997..5fcdc3ac 100644 --- a/apps/sel4test-tests/src/tests/cache.c +++ b/apps/sel4test-tests/src/tests/cache.c @@ -430,7 +430,6 @@ static int test_cache_kernel_only(env_t env) test_error_eq(err, seL4_NoError); /* Page-level operations */ err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); - printf("kernel_only: page clean err: 0x%lx\n", err); test_error_eq(err, seL4_NoError); err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_IllegalOperation); From 13b9de78f3d04e4f97f359354b193b3a321ecd92 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 20 Jun 2024 17:15:34 +1000 Subject: [PATCH 4/4] cache: only expect errors for EL1 armv8-a On armv7-a and in EL-2, the corresponding operations are safe for the kernel to perform. Signed-off-by: Gerwin Klein --- apps/sel4test-tests/src/tests/cache.c | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/apps/sel4test-tests/src/tests/cache.c b/apps/sel4test-tests/src/tests/cache.c index 5fcdc3ac..8582df56 100644 --- a/apps/sel4test-tests/src/tests/cache.c +++ b/apps/sel4test-tests/src/tests/cache.c @@ -386,6 +386,10 @@ static int test_cache_invalid(env_t env) return sel4test_get_result(); } +static inline int CONST invalidate_should_fail() { + return config_set(CONFIG_ARCH_AARCH64) && !config_set(CONFIG_ARM_HYPERVISOR_SUPPORT); +} + static int test_cache_kernel_only(env_t env) { /* @@ -423,7 +427,7 @@ static int test_cache_kernel_only(env_t env) err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, invalidate_should_fail() ? seL4_IllegalOperation : seL4_NoError); err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); @@ -432,7 +436,7 @@ static int test_cache_kernel_only(env_t env) err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, invalidate_should_fail() ? seL4_IllegalOperation : seL4_NoError); err = seL4_ARM_Page_CleanInvalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K); @@ -525,7 +529,7 @@ static int test_cache_read_only(env_t env) err = seL4_ARCH_PageDirectory_Clean_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARCH_PageDirectory_Invalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, invalidate_should_fail() ? seL4_IllegalOperation : seL4_NoError); err = seL4_ARCH_PageDirectory_CleanInvalidate_Data(env->page_directory, vstart, vstart + PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARCH_PageDirectory_Unify_Instruction(env->page_directory, vstart, vstart + PAGE_SIZE_4K); @@ -534,7 +538,7 @@ static int test_cache_read_only(env_t env) err = seL4_ARM_Page_Clean_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARM_Page_Invalidate_Data(frame, 0, PAGE_SIZE_4K); - test_error_eq(err, seL4_IllegalOperation); + test_error_eq(err, invalidate_should_fail() ? seL4_IllegalOperation : seL4_NoError); err = seL4_ARM_Page_CleanInvalidate_Data(frame, 0, PAGE_SIZE_4K); test_error_eq(err, seL4_NoError); err = seL4_ARM_Page_Unify_Instruction(frame, 0, PAGE_SIZE_4K);