[3] Wasm block parameters keep the incoming type instead of the declared one

HighJSC WebAssembly front-endTypeConfusion

9dcbd25

High로 평가한 이유는 다음과 같습니다. validator는 loop의 back edge로 들어오는 값을 선언된 parameter 타입 기준으로 통과시킵니다. 반면 body는 fall-in edge로 들어온 더 좁은 타입에 맞춰 검증되고, 그 타입으로 컴파일된 상태입니다. 새로 추가된 첫 번째 테스트는 임의의 host 값을 구체적인 struct 타입 기준으로 검증된 struct.get까지 밀어 넣습니다. 다만 branch target 쪽 절반은 branch typing 코드를 직접 확인한 결과가 아니라, 스펙 semantics와 테스트 설계에서 따라 나오는 부분입니다.

WebAssembly의 structured control instruction은 parameter를 받을 수 있습니다. 그래서 block의 body로 들어가는 경로가 하나가 아닙니다. fall-in edge가 있고, 그 label을 target으로 삼는 모든 branch 역시 진입 경로가 됩니다. JSC의 single-pass validator인 Wasm::FunctionParser는 이 body를 타입이 붙은 값들의 abstract stack에 대해 단 한 번만 검사합니다. 동시에 같은 pass가 addBlock / addLoop / addIf / addTry를 거쳐 LLInt, BBQ, OMG tier의 code generator를 구동합니다. 스펙에서 block 진입 규칙은 push_ctrl(op, in, out)이 push_vals(in)을 수행하는 형태로 정의되어 있습니다. 즉 선언된 parameter 타입을 push합니다. 이렇게 하면 body는 모든 entry edge가 통과 기준으로 삼는 계약에 대해 검사됩니다. 먼저 도착한 값의 타입이 기준이 되지는 않습니다.

관전 포인트: 웹 페이지가 struct를 들고 loop (param anyref)에 진입하면, body는 그 구체적인 struct 타입에 맞춰 컴파일됩니다. 이후 back edge로 임의의 host 값을 전달하면, 실제 struct 기준으로 검증된 struct.get에 그 값이 도달합니다.

Patch Details

패치 이전에는 모든 block entry handler가 자체 loop를 돌면서 arity를 확인하고 isSubtype(incomingType, declaredParamType)을 검사했습니다. 검사가 끝나면 stack slot에는 더 좁은 incoming 타입이 그대로 남았습니다. 어디에도 setType 호출은 없었습니다. 이번 commit에서는 이 loop들이 제거되었고, 선언된 parameter 타입을 entry stack에 투영하는 공용 코드로 대체되었습니다. 같은 변경이 compare와 if를 결합한 두 fast path, 즉 binaryCompareCase와 unaryCompareCase에도 적용되었습니다. 두 곳 모두 arity 검사와 subtype 검사를 합친 loop를 각자 복사해 들고 있었기 때문입니다.

exit 쪽에서는 선언된 result 타입으로의 widening이 이미 존재했습니다. 다만 fallthrough == MergePoint 조건에 묶여 있었습니다. 그 결과 Else, Catch, CatchAll, 그리고 if의 End fallthrough 경로는 widening 대상에서 빠져 있었습니다. 이번 수정으로 이 경로들도 함께 widening을 수행합니다.

block 진입 시 선언된 parameter 타입 대신 들어온 값의 구체 타입을 기록해, 진입 경로가 여러 개인 body를 한 edge에 맞춰 특수화한 패턴.

Background

이 코드가 있는 위치. Source/JavaScriptCore/wasm/WasmFunctionParser.h의 FunctionParser는 abstract stack 기반의 single-pass typechecker입니다. function body를 검증하면서 동시에 IR generator를 구동합니다. slot마다 갖는 TypedExpression::type()은 검증 상태인 동시에, 각 tier로 전달되는 정적 타입이기도 합니다.

Block parameter와 다중 진입 body. multi-value proposal 이후로 block은 parameter 타입을 선언할 수 있게 되었습니다. 진입 시점에 바깥 stack에서 값을 pop해 가져오는 방식입니다. 특히 loop가 흥미로운 경우입니다. loop label을 대상으로 하는 br은 loop로 다시 진입하기 때문입니다. 그래서 body가 갖는 entry edge 개수는 back edge 개수에 1을 더한 값이 됩니다.

Type widening. GC 타입이 들어오면서 Wasm에도 subtype lattice가 생겼습니다. widening은 어떤 edge가 전달한 구체적인 subtype 대신, 해당 slot에 선언된 supertype을 노출하는 동작입니다. 이런 투영이 존재하는 이유는, 모든 edge에 대해 성립하는 상한 기준으로 body를 한 번만 검사하기 위해서입니다.

정적 속성으로서의 nullability. (ref $0)과 (ref null $0)은 서로 다른 타입입니다. JSC의 struct accessor는 정적 nullability를 컴파일 시점 입력으로 취급해, null check를 생성할지 여부를 결정합니다.

Analysis

widening이 빠지면, validator가 보는 block parameter 타입은 다른 entry edge들이 통과 기준으로 삼는 타입 계약보다 항상 더 좁아집니다. 진입 경로가 하나뿐인 block이나 if에서는 스펙 위반이긴 해도 실질적인 위험으로 이어지지 않습니다. 반면 loop에서는 unsound한 상태가 됩니다. 스펙상 loop label을 향한 branch는 loop가 선언한 parameter 타입 기준으로 검사됩니다. 그런데 패치 이전의 body는 fall-in edge로 들어온 값의 타입에 맞춰 검사되고, 그대로 컴파일되었습니다. branch target 쪽 타입 검사 코드인 unifyControl과 Br/BrIf handler는 제공된 소스에 포함되어 있지 않습니다. 그래서 이 절반은 스펙 semantics와 새로 추가된 테스트의 설계에서 따라 나오는 내용입니다.

새로 추가된 loop-param-type-widening.js가 두 가지 어긋남을 모두 짚어냅니다.

Part 1은 loop (param anyref)를 선언한 뒤 (ref $0) struct를 들고 진입합니다. 패치 이전에는 entry 경로가 해당 slot을 (ref $0) 상태로 남겨두었습니다.
그 타입 아래에서는 struct.get 0 0이 타입 검사를 통과합니다. operand 규칙이 (ref null $0) 또는 그 subtype을 요구하기 때문입니다. 테스트 주석에도 수정 이전에는 해당 module이 통과되었다고 기록되어 있습니다.
back edge에서는 externref에 any.convert_extern을 적용한 값을 push합니다. 타입 0의 struct가 아닌, 임의의 host 값입니다.
이 값이 구체적인 struct 타입 기준으로 검증된 field access까지 도달합니다.

Part 2는 nullability 쪽 변형을 다룹니다. loop는 (param (ref null $0))을 선언하지만, 진입은 non-null인 (ref $0)으로 이루어집니다. 그래서 패치 이전의 body는 non-nullable 타입을 기준으로 삼았습니다. 테스트는 수정 이후 back edge로 전달된 ref.null none이 정상적으로 WebAssembly.RuntimeError를 발생시킨다고 확인합니다. JSC의 struct accessor lowering이 operand의 정적 nullability를 기준으로 null check 생성 여부를 결정한다는 의미가 됩니다. 다만 해당 lowering 코드는 제공된 context에 포함되어 있지 않습니다. 이 추론은 codegen을 직접 확인한 결과가 아니라 테스트 설계에서 나온 것입니다.

exploitability는 이번 호에 실린 다른 widening 버그들과 같은 경로를 따릅니다. validator가 하위 단계로 넘기는 primitive는, 타입 검사를 한 번도 거치지 않은 값에 대한 field access입니다. Part 1의 구성에서는 externref를 통해 페이지가 그 값을 직접 제어합니다. 그래서 field address 계산이 attacker가 고른 비트를 대상으로 수행됩니다. 이번 변경으로 확인되는 범위는 type confusion 자체까지입니다. 이를 read나 write primitive로 발전시키려면, 혼동된 field offset이 어디에 떨어지는지까지 제어할 수 있어야 합니다.

동일하게 widening이 빠진 loop가 모든 block entry handler에 복제되어 있었고, 결합된 두 compare 경로에도 그대로 남아 있었습니다. 발견 경로를 짐작할 수 있는 지점입니다. 한 곳만 고친 수정이라기보다는, entry handler 전반을 패턴 단위로 점검한 결과로 읽힙니다.

Audit directions

진입 쪽 타입 투영과 종료 쪽 widening. exit 경로에는 widening이 있었지만 fallthrough tag 하나에 묶여 있었고, entry 경로에는 아예 없었습니다. structured control instruction마다 두 방향을 각각 따로 확인할 필요가 있습니다. End에서 widening이 정확하게 동작한다고 해서, 그 construct의 entry가 무엇을 기록했는지까지 말해주지는 않습니다.
fast path 안에 복사된 검증 loop. binaryCompareCase와 unaryCompareCase는 compare와 if를 하나로 묶기 때문에, arity 검사와 subtype 검사를 합친 loop를 각자 따로 들고 있었습니다. 재사용 가능한 패턴은 이렇게 opcode를 결합한 fast path가 slow path의 검증 로직을 inline으로 다시 구현하는 형태입니다. WasmFunctionParser.h에서 표준 block handler 바깥에 있는 arity loop를 검색해 볼 만합니다. 코드 리뷰에서의 단서는 signature.argumentCount()를 도는 for loop 안에서 isSubtype만 호출하고 setType은 없는 경우입니다.
스펙 push_ctrl 준수 여부를 체크리스트로. validator의 구현 형태가 스펙의 push_ctrl(op, in, out) / push_vals(in) 정식화에서 벗어나는 지점을 찾고, 그 차이 자체를 정당화 대상으로 두는 방식입니다. 진입 시점에 선언된 in 타입이 아닌 다른 것을 push하는 construct는 모두 후보가 됩니다.