1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#include <assert.h> 14#include <stdio.h> 15#include <stdlib.h> 16#include <sel4/sel4.h> 17#include <vka/object.h> 18 19#include "../helpers.h" 20 21 22#define MAGIC1 42 23#define MAGIC2 0xDEADBEEF 24#define MAGIC3 666 25 26static int check_recv(seL4_CPtr ep, seL4_Word val, seL4_CPtr reply) 27{ 28 api_recv(ep, NULL, reply); 29 test_check(val == seL4_GetMR(0)); 30 // This one is just for Rendez-vous 31 api_recv(ep, NULL, reply); 32 return sel4test_get_result(); 33} 34 35static int test_send_needs_write(env_t env) 36{ 37 vka_t *vka = &env->vka; 38 seL4_CPtr ep = vka_alloc_endpoint_leaky(vka); 39 seL4_CPtr reply = vka_alloc_reply_leaky(vka); 40 seL4_CPtr epMint; 41 vka_cspace_alloc(vka, &epMint); 42 helper_thread_t t; 43 seL4_CapRights_t rights; 44 for (seL4_Word i = 0 ; i < BIT(seL4_MsgExtraCapBits) ; i++) { 45 rights.words[0] = i; 46 create_helper_thread(env, &t); 47 start_helper(env, &t, (helper_fn_t)check_recv, ep, MAGIC1, reply, 0); 48 cnode_mint(env, ep, epMint, rights, 0); 49 50 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 51 if (!seL4_CapRights_get_capAllowWrite(rights)) { 52 seL4_SetMR(0, MAGIC2); 53 seL4_Send(epMint, tag); 54 } 55 seL4_SetMR(0, MAGIC1); 56 seL4_Send(ep, tag); 57 // This one is just for Rendez-vous 58 seL4_Send(ep, tag); 59 cleanup_helper(env, &t); 60 cnode_delete(env, epMint); 61 62 } 63 return sel4test_get_result(); 64} 65 66DEFINE_TEST(IPCRIGHTS0001, "seL4_Send needs write", test_send_needs_write, true) 67 68 69static int 70test_recv_needs_read(env_t env) 71{ 72 vka_t *vka = &env->vka; 73 seL4_CPtr ep = vka_alloc_endpoint_leaky(vka); 74 seL4_CPtr reply = vka_alloc_reply_leaky(vka); 75 seL4_CPtr fault_ep = vka_alloc_endpoint_leaky(vka); 76 seL4_CPtr fault_reply = vka_alloc_reply_leaky(vka); 77 seL4_CPtr epMint; 78 vka_cspace_alloc(vka, &epMint); 79 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 80 for (seL4_Word i = 0 ; i < BIT(seL4_MsgExtraCapBits) ; i++) { 81 seL4_CapRights_t rights; 82 rights.words[0] = i; 83 cnode_mint(env, ep, epMint, rights, 0); 84 helper_thread_t t; 85 create_helper_thread(env, &t); 86 int error; 87 error = api_tcb_set_space(get_helper_tcb(&t), 88 fault_ep, 89 env->cspace_root, 90 seL4_NilData, 91 env->page_directory, seL4_NilData); 92 test_error_eq(error, seL4_NoError); 93 start_helper(env, &t, (helper_fn_t)check_recv, epMint, MAGIC1, reply, 0); 94 95 if (seL4_CapRights_get_capAllowRead(rights)) { 96 seL4_SetMR(0, MAGIC1); 97 seL4_Send(ep, tag); 98 seL4_Send(ep, tag); 99 } else { 100 api_recv(fault_ep, NULL, fault_reply); 101 } 102 cleanup_helper(env, &t); 103 cnode_delete(env, epMint); 104 } 105 106 return sel4test_get_result(); 107} 108 109DEFINE_TEST(IPCRIGHTS0002, "seL4_Recv needs read", test_recv_needs_read, true) 110 111static int 112check_recv_cap(env_t env, seL4_CPtr ep, bool should_recv_cap, seL4_CPtr reply) 113{ 114 vka_t *vka = &env->vka; 115 116 seL4_CPtr recvSlot; 117 int vka_error = vka_cspace_alloc(vka, &recvSlot); 118 test_error_eq(vka_error, seL4_NoError); 119 set_cap_receive_path(env, recvSlot); 120 api_recv(ep, NULL, reply); 121 122 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 123 124 test_assert(seL4_GetMR(0) == MAGIC1); 125 126 if (should_recv_cap) { 127 test_assert(!is_slot_empty(env, recvSlot)); 128 seL4_SetMR(0, MAGIC2); 129 seL4_Send(recvSlot, tag); 130 int error = cnode_delete(env, recvSlot); 131 test_check(!error); 132 } 133 test_assert(is_slot_empty(env, recvSlot)); 134 vka_cspace_free(vka, recvSlot); 135 seL4_SetMR(0, MAGIC3); 136 seL4_Send(ep, tag); 137 138 return sel4test_get_result(); 139} 140 141static int test_send_cap_needs_grant(env_t env) 142{ 143 vka_t *vka = &env->vka; 144 seL4_CPtr ep = vka_alloc_endpoint_leaky(vka); 145 seL4_CPtr reply = vka_alloc_reply_leaky(vka); 146 seL4_CPtr return_ep = vka_alloc_endpoint_leaky(vka); 147 seL4_CPtr return_reply = vka_alloc_reply_leaky(vka); 148 seL4_CPtr epMint; 149 vka_cspace_alloc(vka, &epMint); 150 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 1, 1); 151 152 for (seL4_Word i = 0; i < BIT(seL4_MsgExtraCapBits); i++) { 153 seL4_CapRights_t rights; 154 rights.words[0] = i; 155 if (!seL4_CapRights_get_capAllowWrite(rights)) { 156 continue; 157 } 158 bool grant = seL4_CapRights_get_capAllowGrant(rights); 159 160 cnode_mint(env, ep, epMint, rights, 0); 161 162 helper_thread_t t; 163 create_helper_thread(env, &t); 164 start_helper(env, &t, (helper_fn_t)check_recv_cap, (seL4_Word)env, ep, grant, reply); 165 166 seL4_SetMR(0, MAGIC1); 167 seL4_SetCap(0, return_ep); 168 seL4_Send(epMint, tag); 169 170 if (grant) { 171 api_recv(return_ep, NULL, return_reply); 172 test_check(seL4_GetMR(0) == MAGIC2); 173 } 174 api_recv(ep, NULL, reply); 175 test_check(seL4_GetMR(0) == MAGIC3); 176 cleanup_helper(env, &t); 177 cnode_delete(env, epMint); 178 } 179 180 /* test_check(seL4_GetMR(0) == 42); */ 181 return sel4test_get_result(); 182} 183 184DEFINE_TEST(IPCRIGHTS0003, "seL4_Send with caps needs grant", test_send_cap_needs_grant, true) 185 186#ifndef CONFIG_KERNEL_MCS 187 188static int 189check_call(env_t env, seL4_CPtr ep, bool should_call, bool reply_recv) 190{ 191 vka_t *vka = &env->vka; 192 193 194 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 195 seL4_SetMR(0, MAGIC1); 196 seL4_Call(ep, tag); 197 if (reply_recv) { 198 seL4_Call(ep, tag); 199 } 200 201 202 /* if we are here, the call should have worked (or else we would have been inactive) */ 203 test_assert(should_call); 204 test_assert(seL4_GetMR(0) == MAGIC2); 205 seL4_Send(ep, tag); 206 207 return sel4test_get_result(); 208} 209 210 211 212static int test_call_needs_grant_or_grant_reply(env_t env) 213{ 214 vka_t *vka = &env->vka; 215 seL4_CPtr ep = vka_alloc_endpoint_leaky(vka); 216 seL4_CPtr return_ep = vka_alloc_endpoint_leaky(vka); 217 seL4_CPtr reply = get_free_slot(env); 218 seL4_CPtr epMint = get_free_slot(env); 219 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 220 221 enum { 222 nothing, 223 save_caller, 224 reply_recv 225 }; 226 227 for (int mode = nothing; mode <= reply_recv; mode++) { 228 for (seL4_Word i = 0; i < BIT(seL4_MsgExtraCapBits); i++) { 229 seL4_CapRights_t rights; 230 rights.words[0] = i; 231 if (!seL4_CapRights_get_capAllowWrite(rights)) { 232 continue; 233 } 234 bool grant = seL4_CapRights_get_capAllowGrant(rights); 235 bool grant_reply = seL4_CapRights_get_capAllowGrantReply(rights); 236 237 cnode_copy(env, ep, epMint, rights); 238 239 helper_thread_t t; 240 create_helper_thread(env, &t); 241 start_helper(env, &t, (helper_fn_t)check_call, (seL4_Word)env, epMint, 242 grant || grant_reply, mode == reply_recv); 243 244 245 seL4_Recv(ep, NULL); 246 if (grant || grant_reply) { 247 test_check(seL4_GetMR(0) == MAGIC1); 248 switch (mode) { 249 case nothing: 250 seL4_SetMR(0, MAGIC2); 251 seL4_Reply(tag); 252 cnode_savecaller(env, reply); 253 test_assert(is_slot_empty(env, reply)); 254 break; 255 case save_caller: 256 cnode_savecaller(env, reply); 257 test_assert(!is_slot_empty(env, reply)); 258 seL4_SetMR(0, MAGIC2); 259 seL4_Send(reply, tag); 260 test_assert(is_slot_empty(env, reply)); 261 break; 262 case reply_recv: 263 seL4_ReplyRecv(ep, tag, NULL); 264 seL4_SetMR(0, MAGIC2); 265 seL4_Reply(tag); 266 cnode_savecaller(env, reply); 267 test_assert(is_slot_empty(env, reply)); 268 break; 269 } 270 seL4_Recv(ep, NULL); 271 test_check(seL4_GetMR(0) == MAGIC2); 272 } else { 273 cnode_savecaller(env, reply); 274 test_assert(is_slot_empty(env, reply)); 275 cnode_delete(env, epMint); 276 cnode_copy(env, ep, epMint, seL4_AllRights); 277 seL4_TCB_Resume(get_helper_tcb(&t)); 278 seL4_Recv(ep, NULL); 279 cnode_savecaller(env, reply); 280 test_assert(!is_slot_empty(env, reply)); 281 seL4_TCB_Suspend(get_helper_tcb(&t)); 282 test_assert(is_slot_empty(env, reply)); 283 } 284 cleanup_helper(env, &t); 285 cnode_delete(env, epMint); 286 } 287 } 288 289 return sel4test_get_result(); 290} 291 292DEFINE_TEST(IPCRIGHTS0004, "seL4_Call needs grant or grant-reply", 293 test_call_needs_grant_or_grant_reply, true) 294 295static int 296check_call_return_cap(env_t env, seL4_CPtr ep, 297 bool should_recv_cap, bool reply_recv) 298{ 299 vka_t *vka = &env->vka; 300 301 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 1); 302 seL4_CPtr recvSlot = get_free_slot(env); 303 set_cap_receive_path(env, recvSlot); 304 seL4_SetMR(0, MAGIC1); 305 seL4_Call(ep, tag); 306 if (reply_recv) { 307 seL4_Call(ep, tag); 308 } 309 310 test_check(seL4_GetMR(0) == MAGIC2); 311 312 if (should_recv_cap) { 313 test_assert(!is_slot_empty(env, recvSlot)); 314 seL4_SetMR(0, MAGIC3); 315 seL4_Send(recvSlot, tag); 316 int error = cnode_delete(env, recvSlot); 317 test_check(!error); 318 } 319 test_assert(is_slot_empty(env, recvSlot)); 320 vka_cspace_free(vka, recvSlot); 321 seL4_SetMR(0, MAGIC3); 322 seL4_Send(ep, tag); 323 return sel4test_get_result(); 324} 325 326static int test_reply_grant_receiver(env_t env) 327{ 328 vka_t *vka = &env->vka; 329 seL4_CPtr ep = vka_alloc_endpoint_leaky(vka); 330 seL4_CPtr return_ep = vka_alloc_endpoint_leaky(vka); 331 seL4_CPtr reply = get_free_slot(env); 332 seL4_CPtr epMint = get_free_slot(env); 333 seL4_MessageInfo_t tag_no_cap = seL4_MessageInfo_new(0, 0, 0, 1); 334 seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 1, 1); 335 336 enum { 337 nothing, 338 save_caller, 339 reply_recv 340 }; 341 342 for (int mode = nothing; mode <= reply_recv; mode++) { 343 for (seL4_Word i = 0; i < BIT(seL4_MsgExtraCapBits); i++) { 344 seL4_CapRights_t rights; 345 rights.words[0] = i; 346 if (!seL4_CapRights_get_capAllowRead(rights)) { 347 continue; 348 } 349 bool grant = seL4_CapRights_get_capAllowGrant(rights); 350 351 cnode_copy(env, ep, epMint, rights); 352 353 helper_thread_t t; 354 create_helper_thread(env, &t); 355 start_helper(env, &t, (helper_fn_t)check_call_return_cap, 356 (seL4_Word)env, ep, grant, mode == reply_recv); 357 358 seL4_Recv(epMint, NULL); 359 seL4_Word callmsg = seL4_GetMR(0); 360 test_check(callmsg == MAGIC1); 361 if (mode == save_caller) { 362 cnode_savecaller(env, reply); 363 test_assert(!is_slot_empty(env, reply)); 364 seL4_SetMR(0, MAGIC2); 365 seL4_SetCap(0, return_ep); 366 seL4_Send(reply, tag); 367 test_assert(is_slot_empty(env, reply)); 368 } else { 369 if (mode == reply_recv) { 370 seL4_ReplyRecv(epMint, tag_no_cap, NULL); 371 } 372 seL4_SetMR(0, MAGIC2); 373 seL4_SetCap(0, return_ep); 374 seL4_Reply(tag); 375 } 376 377 if (grant) { 378 seL4_Recv(return_ep, NULL); 379 test_check(seL4_GetMR(0) == MAGIC3); 380 } 381 seL4_Recv(ep, NULL); 382 test_check(seL4_GetMR(0) == MAGIC3); 383 cleanup_helper(env, &t); 384 cnode_delete(env, epMint); 385 } 386 } 387 388 return sel4test_get_result(); 389} 390 391DEFINE_TEST(IPCRIGHTS0005, "seL4_Reply grant depends of the grant of previous seL4_Recv", 392 test_reply_grant_receiver, true) 393 394 395 396 397#endif /* CONFIG_KERNEL_MCS */ 398 399