move: capability가 struct 필드로 복제되던 구멍을 막는다 (보안 정리 ii)
"발견들 다 고쳤나"를 확인하려고 전부 다시 돌려보다 드러났다.
pub struct Wrapper { pay: Pay }
pub fn duplicate(w: Wrapper) effects {Pay.charge} {
consume(w.pay)
consume(w.pay) // 같은 capability를 두 번 소비 — 통과했다
}
w가 빌린 값인데도 통과했다. 즉 "safe code에서 capability는 복제·위조되지
않는다"가 깨져 있었다. 이 세션에서 찾은 것 중 가장 심각하다.
원인은 단순하다. E_field가 빌린 값을 돌려주는데 Move 문맥에서 그것을
검사하는 곳이 E_ident 분기에만 있었고, 필드 접근은 그 분기를 지나가지
않는다. 규칙("v0에 부분 move는 없다")은 주석에 적혀 있었으나 강제되지
않았다.
필드의 affinity를 알아야 정확히 막을 수 있어서 move 검사기에 struct 필드
표와 바인딩의 선언 타입을 넣었다. copyable 필드는 막지 않는다 — w.label은
통과한다.
이것이 LRU에서 열거형으로 우회한 것을 사후에 정당화한다. 그때는 "struct로는
안 되고 열거형으로는 된다"가 우연처럼 보였는데, 열거형이 유일한 길인 것이
규칙이었고 struct 쪽이 새고 있었을 뿐이다.
여태 안 보인 이유: samples/05는 자원 타입을 직접 다루고 struct에 담지
않는다. 개밥 먹기에서 자원을 자료구조에 담는 코드를 처음 쓰면서 드러났다.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019ZVDeU6KLuUVL3gs18Hm3E
This commit is contained in:
Claude Opus 5
+48
-1
@@ -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다.
|
||||
|
||||
|
||||
+52
-11
@@ -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 = [];
|
||||
|
||||
@@ -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}") = [])
|
||||
|
||||
Reference in New Issue
Block a user