[WIP] tree authorization

examples/.gitignore

@@ -34,3 +34,4 @@
 /bad_overlap_ASID
 /bad_overlap_VMID
 /bad_EL2_ASID
+/bad_no_write_auth

examples/Makefile

@@ -21,6 +21,7 @@ build-objs += good_bbm_stage1
 build-objs += bad_no_bbm_stage1
 build-objs += bad_overlap_ASID
 build-objs += bad_EL2_ASID
+build-objs += bad_no_write_auth
 
 list-build-objs:
 	@echo $(build-objs)

examples/common.c

@@ -22,6 +22,7 @@ bool SHOULD_PRINT_DIFF = false;
 bool SHOULD_PRINT_ONLY_UNCLEANS = true;
 bool SHOULD_CHECK = true;
 bool SHOULD_CHECK_LOCKS = true;
+bool SHOULD_CHECK_AUTH = true;
 bool SHOULD_TRACE = true;
 bool SHOULD_TRACE_CONDENSED = false;
 bool QUIET = false;
@@ -112,6 +113,7 @@ static void print_help_and_quit(void)
 	printf(
 		"Usage: \n"
 		"  -R --racy      	do not check locks/synchronisation are respected\n"
+		"  -A --no-auth  	do not check write-authorization\n"
 		"  -t --trace    	print trace record for each step\n"
 		"  -c            	condensed trace format\n"
 		"  -d --diff     	show diffs of state\n"
@@ -142,11 +144,12 @@ void common_read_argv(int argc, char **argv)
 		{"color",      no_argument, 0,  7 },
 		{"help",       no_argument, 0,  8 },
 		{"racy",       no_argument, 0,  'R' },
+		{"no-auth",   no_argument, 0,  'A' },
 		{0,            0,           0,  0 }
 	};
 
 	int c;
-	while ((c = getopt_long(argc, argv, "acptqdhUR", long_options, 0)) != - 1) {
+	while ((c = getopt_long(argc, argv, "acptqdhURA", long_options, 0)) != - 1) {
 		switch (c) {
 		case 0:
 		case 'p':
@@ -188,6 +191,10 @@ void common_read_argv(int argc, char **argv)
 			SHOULD_CHECK_LOCKS = false;
 			break;
 
+		case 'A':
+			SHOULD_CHECK_AUTH = false;
+			break;
+
 		case 6:
 		case 'a':
 			COLOR = false;
@@ -298,6 +305,7 @@ void common_init(int argc, char **argv)
 
 	opts.check_opts.enable_printing = SHOULD_PRINT_DIFF | SHOULD_PRINT_STATE;
 	opts.check_opts.check_synchronisation = SHOULD_CHECK_LOCKS;
+	opts.check_opts.check_authorization = SHOULD_CHECK_AUTH;
 	opts.check_opts.print_opts = CM_PRINT_NONE;
 	if (SHOULD_PRINT_ONLY_UNCLEANS)
 		opts.check_opts.print_opts |= CM_PRINT_ONLY_UNCLEAN;

examples/expected/bad_no_write_auth.log

@@ -0,0 +1,10 @@
+(mem-init (id 0) (tid 0) (address 0xaaaac17b5000) (size 0x1000) (src "examples/tests/bad_no_write_auth.c:20"))
+(mem-init (id 1) (tid 0) (address 0xaaaac17b6000) (size 0x1000) (src "examples/tests/bad_no_write_auth.c:21"))
+(hint (id 2) (tid 0) (kind set_root_lock) (location 0xaaaac17b5000) (value 0xaaaac17b7000) (src "examples/tests/bad_no_write_auth.c:22"))
+(hint (id 3) (tid 0) (kind set_owner_root) (location 0xaaaac17b6000) (value 0xaaaac17b5000) (src "examples/tests/bad_no_write_auth.c:23"))
+(mem-write (id 4) (tid 0) (mem-order plain) (address 0xaaaac17b5000) (value 0xaaaac17b6003) (src "examples/tests/bad_no_write_auth.c:26"))
+(sysreg-write (id 5) (tid 0) (sysreg vttbr_el2) (value 0xaaaac17b5000) (src "examples/tests/bad_no_write_auth.c:29"))
+(lock (id 6) (tid 0) (address 0xaaaac17b7000) (src "examples/tests/bad_no_write_auth.c:31"))
+(mem-write (id 7) (tid 0) (mem-order plain) (address 0xaaaac17b6000) (value 0x1) (src "examples/tests/bad_no_write_auth.c:32"))
+(mem-write (id 8) (tid 0) (mem-order plain) (address 0xaaaac17b6008) (value 0x1) (src "examples/tests/bad_no_write_auth.c:33"))
+! Wrote plain without authorization

examples/tests/bad_no_write_auth.c

@@ -0,0 +1,35 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdarg.h>
+
+#include "common.h"
+
+/* locations we can pretend are pagetables
+ */
+__attribute__((aligned(4096)))
+u64 root[512];
+u64 child[512];
+u64 l;
+
+int main(int argc, char **argv)
+{
+	common_init(argc, argv);
+
+	/* tell the modle pud and pgd tables exist,
+	 * and logically associate them with the lock. */
+	TRANS_MEM_INIT((u64)root, 4096);
+	TRANS_MEM_INIT((u64)child, 4096);
+	HINT(GHOST_HINT_SET_ROOT_LOCK, (u64)root, (u64)&l);
+	HINT(GHOST_HINT_SET_OWNER_ROOT, (u64)child, (u64)root);
+
+	/* make root[0] point to child */
+	WRITE_ONCE(root[0], (u64)child | 0b11);
+
+	/* track pud as the root */
+	MSR(SYSREG_VTTBR, (u64)root);
+
+	LOCK(l);
+	WRITE_ONCE(child[0], 1);
+	WRITE_ONCE(child[1], 1);
+	UNLOCK(l);
+}

src/casemate-check-c/include/casemate-check-impl.h

@@ -10,6 +10,7 @@ extern bool SHOULD_PRINT_DIFF;
 extern bool SHOULD_PRINT_ONLY_UNCLEANS;
 extern bool SHOULD_CHECK;
 extern bool SHOULD_CHECK_LOCKS;
+extern bool SHOULD_CHECK_AUTH;
 extern bool SHOULD_TRACK_ONLY_WATCHPOINTS;
 extern bool SHOULD_TRACE;
 extern bool SHOULD_TRACE_CONDENSED;

src/casemate-check-c/src/driver.c

@@ -126,6 +126,7 @@ void *initialise_casemate(void)
 	/* TODO: for now ... */
 	opts.check_opts.promote_TLBI_by_id = true;
 	opts.check_opts.check_synchronisation = SHOULD_CHECK_LOCKS;
+	opts.check_opts.check_authorization = SHOULD_CHECK_AUTH;
 
 	opts.enable_tracing = SHOULD_TRACE;
 

src/casemate-check-c/src/opts.c

@@ -12,6 +12,7 @@ bool SHOULD_PRINT_DIFF = false;
 bool SHOULD_PRINT_ONLY_UNCLEANS = true;
 bool SHOULD_CHECK = true;
 bool SHOULD_CHECK_LOCKS = true;
+bool SHOULD_CHECK_AUTH = true;
 bool SHOULD_TRACK_ONLY_WATCHPOINTS = false;
 bool SHOULD_TRACE = true;
 bool SHOULD_TRACE_CONDENSED = false;
@@ -30,6 +31,7 @@ static void print_help_and_quit(void)
 		"\n"
 		"Options:\n"
 		"  -R --racy      	do not check locks/synchronisation are respected\n"
+		"  -A --no-auth   	do not check for write-authorization\n"
 		"  -t --trace     	print trace record for each step\n"
 		"  -T --no-trace  	do not print trace record for each step\n"
 		"  -c             	condensed trace format\n"
@@ -71,6 +73,7 @@ void parse_opts(int argc, char **argv)
 		{"all",        no_argument, 0,  'U' },
 		{"dry-run",    no_argument, 0,  'C' },
 		{"racy",       no_argument, 0,  'R' },
+		{"no-auth",      no_argument, 0,  'A' },
 		{"no-color",  no_argument, 0,  'a' },
 		{"color",     no_argument, 0,  'G' },
 		{"debug",      no_argument, 0,  'D' },
@@ -80,7 +83,7 @@ void parse_opts(int argc, char **argv)
 	};
 
 	int c;
-	while ((c = getopt_long(argc, argv, "acptTqdhUDRVW:", long_options, 0)) != - 1) {
+	while ((c = getopt_long(argc, argv, "acptTqdhUDRAVW:", long_options, 0)) != - 1) {
 		switch (c) {
 		case 'p':
 			SHOULD_PRINT_STATE = true;
@@ -122,6 +125,10 @@ void parse_opts(int argc, char **argv)
 			SHOULD_CHECK_LOCKS = false;
 			break;
 
+		case 'A':
+			SHOULD_CHECK_AUTH = false;
+			break;
+
 		case 'W': {
 			u64 val;
 			if (optarg[0] != '0' || optarg[1] != 'x') {

src/lib/casemate.h

@@ -79,6 +79,11 @@ struct casemate_checker_options {
 	 */
 	bool check_synchronisation;
 
+	/**
+	 * @check_authorization: check that write-authorizations are respected.
+	 */
+	bool check_authorization;
+
 	/**
 	 * @enable_printing: print out the current state of the
 	 * @print_opts: logging to perform.
@@ -93,6 +98,7 @@ struct casemate_checker_options {
 		.promote_TLBI_nsh = false, \
 		.promote_TLBI_by_id = false, \
 		.check_synchronisation = true, \
+		.check_authorization = true, \
 		.enable_printing = false, \
 		.print_opts = CASEMATE_DEFAULT_PRINT_OPTS, \
 	}

src/lib/include/casemate-in/casemate-config.in.h

@@ -42,6 +42,11 @@ struct casemate_checker_options {
 	 */
 	bool check_synchronisation;
 
+	/**
+	 * @check_authorization: check that write-authorizations are respected.
+	 */
+	bool check_authorization;
+
 	/**
 	 * @enable_printing: print out the current state of the
 	 * @print_opts: logging to perform.
@@ -56,6 +61,7 @@ struct casemate_checker_options {
 		.promote_TLBI_nsh = false, \
 		.promote_TLBI_by_id = false, \
 		.check_synchronisation = true, \
+		.check_authorization = true, \
 		.enable_printing = false, \
 		.print_opts = CASEMATE_DEFAULT_PRINT_OPTS, \
 	}

src/lib/src/model.c

@@ -846,7 +846,7 @@ static void check_write_is_authorized(struct sm_location *loc, struct ghost_hw_s
 
 	/* if synchronisation is disabled, then cannot check write authorization
 	 * as it comes from the synchronisation itself */
-	if (!opts()->check_opts.check_synchronisation)
+	if (!opts()->check_opts.check_synchronisation || !opts()->check_opts.check_authorization)
 		return;
 
 	// if the location is owned by a given thread, just test if it is this one