diff --git a/dogfoods/FINDINGS.md b/dogfoods/FINDINGS.md index 0290697..3f73767 100644 --- a/dogfoods/FINDINGS.md +++ b/dogfoods/FINDINGS.md @@ -314,7 +314,54 @@ pub fn probe3(r: Result[Int, String]) -> String { 같은 코드는 v가 TUnknown이어도 통과하므로 **아무도 이상함을 못 느낀다.** 틀린 코드를 써봐야 드러난다. -### D11. struct 필드에서 affine 값을 꺼낼 수 없다 +### D11. struct 필드와 affine 값 — 그리고 여기서 보안 구멍이 나왔다 + +처음 이렇게 적었다: "필드 접근은 빌림이라 affine 값을 꺼낼 수 없다." +**규칙으로는 맞았는데 구현이 그것을 강제하지 않고 있었다.** + +나중에 "다 고쳤나"를 확인하려고 전부 다시 돌려보다 드러났다: + +```cool +pub capability Pay { fn charge(n: Int) effects {Pay.charge} } +pub struct Wrapper { pay: Pay } +pub fn consume(own p: Pay) effects {Pay.charge} + +pub fn duplicate(w: Wrapper) effects {Pay.charge} { + consume(w.pay) + consume(w.pay) // 같은 capability를 두 번 소비한다 +} +``` + +**통과했다.** 그것도 `w`가 **빌린 값**인데도. 즉 **보안 정리 (ii)("safe +code에서 capability는 복제·위조되지 않는다")가 깨져 있었다.** 이 세션에서 +찾은 것 중 가장 심각하다. + +원인: `E_field`가 빌린 값(`v_use = true`)을 돌려주는데, **`Move` 문맥에서 +그것을 검사하는 곳이 `E_ident` 분기에만 있었다.** 필드 접근은 그 분기를 +지나가지 않는다. + +고쳤다. `E_field`가 Move 자리에 놓이고 필드가 affine이면 오류다: + +``` +pay 필드는 affine이라 다른 함수에 넘길 수 없습니다 +(v0에는 부분 move가 없습니다 — 꺼내려면 열거형으로 감싸십시오) +``` + +필드의 affinity를 알려면 바인딩의 선언 타입이 필요해서, move 검사기에 +struct 필드 표와 바인딩 타입을 넣었다. **copyable 필드는 막지 않는다** — +`w.label`은 통과한다. + +그리고 이것이 LRU에서 열거형으로 우회한 것을 사후에 정당화한다. 그때는 +"struct로는 안 되고 열거형으로는 된다"가 우연처럼 보였는데, **열거형이 +유일한 길인 것이 규칙이었고 struct 쪽이 새고 있었을 뿐이다.** + +#### 이 버그가 여태 안 보인 이유 + +`samples/05_move_errors.cool`은 자원 타입을 **직접** 다룬다. struct에 넣고 +필드로 꺼내는 코드가 없었다. 개밥 먹기에서 **자원을 자료구조에 담는** 코드를 +처음 쓰면서 드러났다. + +#### (원래 기록) 열거형으로만 둘을 함께 돌려줄 수 있다 `put`은 캐시와 축출된 자원을 **함께** 돌려줘야 한다. 튜플이 없으니 struct다. diff --git a/lib/move.ml b/lib/move.ml index 9285469..86a8978 100644 --- a/lib/move.ml +++ b/lib/move.ml @@ -27,12 +27,17 @@ type binding = { b_use : bool; b_mut : bool; b_depth : int; + (* 선언된 타입. 필드가 affine인지 알려면 필요하다 — 모르면 필드에서 + 꺼내는 것을 막을 수 없고, 그러면 capability가 struct를 통해 복제된다. *) + b_ty : ty option; } type fninfo = { f_params : param list; f_ret : Ast.ty option } type state = { aff : (string, bool) Hashtbl.t; + (* struct 이름 -> 필드 이름과 타입 *) + fields : (string, (string * ty) list) Hashtbl.t; fns : (string, fninfo) Hashtbl.t; meths : (string, (string * fninfo) list) Hashtbl.t; mutable scopes : binding list list; @@ -78,7 +83,10 @@ let derive_affinity st (items : item list) = (fun it -> match it with | I_capability { name; _ } -> Hashtbl.replace st.aff name true - | I_struct { name; _ } -> Hashtbl.replace st.aff name false + | I_struct { name; fields; _ } -> + Hashtbl.replace st.aff name false; + Hashtbl.replace st.fields name + (List.map (fun f -> (f.f_name, f.f_ty)) fields) | I_enum { name; _ } -> Hashtbl.replace st.aff name false | _ -> ()) items; @@ -126,7 +134,7 @@ let derive_affinity st (items : item list) = let push st = st.scopes <- [] :: st.scopes let pop st = match st.scopes with _ :: r -> st.scopes <- r | [] -> () -let add st name ~affine ~use ~mut_ = +let add st name ~affine ~use ~mut_ ?ty () = st.next_id <- st.next_id + 1; let b = { @@ -136,6 +144,7 @@ let add st name ~affine ~use ~mut_ = b_use = use; b_mut = mut_; b_depth = st.depth; + b_ty = ty; } in (match st.scopes with @@ -188,6 +197,22 @@ let merge st snaps = type ctx = Borrow | Move of string (* 어디로 옮겨가는지 — 진단에 쓴다 *) +(* 필드의 선언된 타입. 바인딩의 타입을 알아야 찾을 수 있다 — 모르면 None이고, + 그때는 객체가 affine인지로 보수적으로 판정한다. *) +let field_ty st (obj : expr) (name : string) : ty option = + match obj with + | E_ident (n, _) -> ( + match find st n with + | Some b -> ( + match b.b_ty with + | Some (T_named { name = tn; _ }) -> ( + match Hashtbl.find_opt st.fields tn with + | Some fs -> List.assoc_opt name fs + | None -> None) + | _ -> None) + | None -> None) + | _ -> None + let rec walk st (ctx : ctx) (e : expr) : vinfo = match e with | E_lit _ -> v_copy @@ -272,7 +297,7 @@ let rec walk st (ctx : ctx) (e : expr) : vinfo = ignore (walk st Borrow (E_ident (parent, Token.{ line = 0; col = 0 }))); push st; (* 자식 TaskScope는 second-class다 — 블록 밖으로 나갈 수 없다 *) - ignore (add st name ~affine:true ~use:true ~mut_:false); + ignore (add st name ~affine:true ~use:true ~mut_:false ()); let r = walk_block st ctx body in pop st; r @@ -282,11 +307,26 @@ let rec walk st (ctx : ctx) (e : expr) : vinfo = pop st; r | E_call { callee; args; pos } -> walk_call st callee args pos - | E_field { obj; _ } -> - (* v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다. *) + | E_field { obj; name; pos } -> + (* v0에 부분 move는 없다. 필드 접근은 빌림이고 결과도 빌린 값이다. + 그러므로 Move 자리에 놓으면 오류다 — 이 검사가 없으면 capability를 + struct에 넣고 필드를 두 번 읽어 복제할 수 있다 (보안 정리 ii). *) let o = walk st Borrow obj in - if o.v_affine || o.v_use then { v_affine = true; v_use = true } - else v_copy + let fa = + match field_ty st obj name with + | Some t -> ty_affine st t + | None -> o.v_affine || o.v_use + in + (match ctx with + | Borrow -> () + | Move where -> + if fa then + err st pos + (Printf.sprintf + "%s 필드는 affine이라 %s 없습니다 (v0에는 부분 move가 없습니다 — 꺼내려면 열거형으로 \ + 감싸십시오)" + name where)); + if fa then { v_affine = true; v_use = true } else v_copy | E_inst { callee; _ } -> walk st Borrow callee | E_try { inner; _ } -> walk st ctx inner | E_unary { operand; _ } -> walk st Borrow operand @@ -299,7 +339,7 @@ and bind_pattern st (info : vinfo) p = match p with | P_wild _ | P_lit _ -> () | P_bind (n, _) -> - ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_:false) + ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_:false ()) | P_ctor { args; _ } -> List.iter (bind_pattern st info) args and walk_block st ctx (b : block) : vinfo = @@ -318,7 +358,7 @@ and walk_stmt st = function let rec bind p = match p with | P_bind (n, _) -> - ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_) + ignore (add st n ~affine:info.v_affine ~use:info.v_use ~mut_ ()) | P_ctor { args; _ } -> List.iter bind args | _ -> () in @@ -355,7 +395,7 @@ and walk_closure st (c : closure) : vinfo = 파라미터를 무조건 소유로 봤고, 그래서 고차 경계에서 소유권 검사가 뚫렸다 (dogfoods/FINDINGS D5). *) let use_ = affine && not p.cp_own in - ignore (add st p.cp_name ~affine ~use:use_ ~mut_:false)) + ignore (add st p.cp_name ~affine ~use:use_ ~mut_:false ?ty:p.cp_ty ())) c.cl_params; ignore (walk_block st (Move "반환할 수") c.cl_body); pop st; @@ -446,7 +486,7 @@ let check_fn st (d : fn_decl) = let affine = ty_affine st p.p_ty in (* 무표기 = 빌림. own만이 소유 이전이다. *) let use_ = affine && not p.p_own in - ignore (add st p.p_name ~affine ~use:use_ ~mut_:p.p_mut)) + ignore (add st p.p_name ~affine ~use:use_ ~mut_:p.p_mut ~ty:p.p_ty ())) d.fn_params; let r = walk_block st (Move "반환할 수") body in (match d.fn_ret with @@ -462,6 +502,7 @@ let check ?(imports : item list = []) (m : modul) : error list = let st = { aff = Hashtbl.create 16; + fields = Hashtbl.create 16; fns = Hashtbl.create 16; meths = Hashtbl.create 16; scopes = []; diff --git a/test/test_coollang.ml b/test/test_coollang.ml index 266a5f9..d31fc84 100644 --- a/test/test_coollang.ml +++ b/test/test_coollang.ml @@ -1732,3 +1732,33 @@ let () = \ }\n\ }" "match 팔의 타입이 서로 다릅니다") + +(* 보안 정리 (ii): safe code에서 capability는 복제되지 않는다. + struct 필드를 통한 구멍이 있었다 — 필드 접근이 빌린 값을 돌려주는데 + Move 자리에서 그것을 검사하는 곳이 없었다. 빌린 wrapper에서도 됐다. *) +let () = + let src = + "capability Pay {\n\ + \ fn charge(n: Int) effects {Pay.charge}\n\ + }\n\n\ + struct Wrapper {\n\ + \ pay: Pay,\n\ + \ label: String,\n\ + }\n\n\ + fn consume(own p: Pay) effects {Pay.charge}\n\n" + in + check "capability를 필드로 복제할 수 없다" + (move_has + (src + ^ "fn duplicate(w: Wrapper) effects {Pay.charge} {\n\ + \ consume(w.pay)\n\ + \ consume(w.pay)\n\ + }") + "부분 move가 없습니다"); + check "소유한 struct에서도 필드를 꺼낼 수 없다" + (move_has + (src + ^ "fn take(own w: Wrapper) effects {Pay.charge} {\n consume(w.pay)\n}") + "부분 move가 없습니다"); + check "copyable 필드는 막지 않는다" + (move_errs (src ^ "fn label_of(w: Wrapper) -> String {\n w.label\n}") = [])