Cedar는 누가 접근할 수 있는지를 증명합니다. 어떤 결정이 내려질지는 누가 증명하나요?

Amazon의 Cedar는 정책 도구가 좀처럼 하지 않는 일을 합니다. 정책을 평가하는 데서 멈추지 않고, 그 정책이 무엇을 보장하는지 증명까지 합니다.

실제 엔지니어링 성과이고, 그게 하필 authorization 영역에서 먼저 나온 데는 이유가 있습니다. 문제의 모양을 보면 납득이 됩니다. 다만 바로 옆에 질문 하나가 그대로 남습니다. 룰 엔진 시장의 누구도 답하지 않은 질문입니다.

접근 허용 여부도 결정의 한 종류입니다. 주문에 적용되는 할인, 대출 신청의 자격 판정, 이체를 막는 사기 임계값, 기능을 여는 요금제 게이트. 이쪽도 전부 결정이고, 매주 바뀌는 건 오히려 이쪽입니다.

이 결정들은 누가 증명하나요?

이 글은 그 공백을 다룹니다. Cedar가 무엇을 어떻게 검증하는지, 비즈니스 결정 규칙이 왜 접근 정책보다 어려운 검증 대상인지, 그리고 LexQ가 여기서 어디에 서 있는지를 차례로 짚습니다. 마지막 답을 먼저 적자면, LexQ가 서 있는 자리는 해법이 아니라 문제 정의입니다.

Cedar가 실제로 증명하는 것

Cedar는 Amazon이 공개한 권한 정책 언어이고, Amazon Verified Permissions의 기반 언어입니다. 정책은 대략 이렇게 생겼습니다.

permit (
  principal in Group::"engineering",
  action == Action::"viewDocument",
  resource in Folder::"internal"
) when {
  resource.classification != "restricted"
};

문법 자체는 넘어가도 됩니다. 중요한 건 Cedar 팀이 그 아래에 무엇을 깔아뒀는가입니다. Cedar의 semantics는 증명 보조 도구인 Lean으로 모델링돼 있고, 언어 자체의 속성은 테스트 스위트가 아니라 기계가 검사한 증명(machine-checked proof)으로 세워져 있습니다. 그 위에 정책 집합 전체를 대상으로 삼는 automated reasoning 도구가 붙습니다. 이 버전이 저 버전과 같은지, 이번 변경이 접근을 더 넓히는 쪽으로 갔는지, 이 정책이 애초에 접근을 허용할 수 있기는 한지를 묻습니다.

테스트 스위트가 답하는 질문이 아닙니다. 테스트는 누군가 적어 둔 입력만 확인해 줍니다. solver는 입력 공간 전체를 확인합니다. 아무도 적어 볼 생각조차 못 한 입력까지 포함해서요.

그러니까 Cedar는 출시된 상용 제품 안에 들어간 formal verification입니다. 실무 관심사를 겨냥했고, 연구자가 아닌 엔지니어가 씁니다. 이 사실은 다른 무엇보다 먼저 분명히 적어야 합니다. 이 글의 나머지가 Cedar가 가지 않은 자리를 이야기하기 때문입니다.

접근 권한과 결과는 다른 질문입니다

권한 결정은 모양이 작고 얌전합니다. principal, action, resource, context가 들어가고 비트 하나가 나옵니다. 허용이거나 거부입니다. 정책에 속성 조건을 아무리 쌓아 올려도 출력은 비트 하나로 유지됩니다. 결합 방식은 언어가 못 박아 둡니다. 정책 작성자에게 선택권이 없습니다. Cedar에서는 명시적 forbid가 어떤 permit보다 우선하고, permit이 없으면 거부입니다.

비즈니스 결정은 모양부터 다릅니다. 이 주문에 어떤 할인이 붙는지 물으면 돌아오는 건 값이고, 그 값은 fact를 읽고 fact를 쓰고 앞선 규칙이 써 둔 것을 다시 읽는 여러 규칙이 함께 만들어 냅니다.

LexQ에서 규칙 하나가 하는 일은 셋 중 하나입니다. fact를 설정하거나, 산술로 바꾸거나, 결정을 아예 차단합니다. 규칙은 버전 안에서 우선순위 순서로 평가되고, 그래서 cartTotal을 바꾸는 규칙 하나가 그 아래 모든 규칙이 보는 입력을 바꿔 놓습니다. mutex group은 한 묶음 안에서 어떤 규칙이 함께 발동할 수 있는지를 제약합니다. 하나만 허용하거나, N개까지 허용합니다. 조건이 비어 있는 규칙은 언제나 적용되는 catch-all입니다.

이걸 쌓아 올리면 결과로 남는 것은 값의 집합, 그 값이 만들어진 순서, 그리고 각 단계가 무엇을 덮어썼는지의 기록입니다. 예전에 의사결정 운영은 authorization이 아니고 OPA나 Cedar 같은 policy-as-code 도구는 접근을 결정한다고 한 줄로 적은 적이 있습니다. 그 한 줄이 짊어진 무게에 비해 설명이 가장 적었던 대목이 여기입니다.

검증 대상도 따라서 달라집니다

접근 정책에서 추론 대상이 되는 객체는 속성 위의 boolean 함수입니다. 그것도 어렵지만, SMT solver가 편안하게 다루는 영역 안에 있습니다. boolean, 집합, 문자열 동등 비교, 정수 비교.

비즈니스 결정 규칙은 그 밖의 것을 전부 끌고 들어옵니다. 우선 비교를 넘어서는 산술이 들어옵니다. 규칙이 곱하고 빼고 상한을 걸기 때문입니다. 순서도 들어옵니다. 우선순위 때문에 7번 규칙은 3번 규칙이 이미 고쳐 놓은 세계를 상대로 평가되고, 그래서 포뮬러는 고정된 조건 묶음 하나가 아니라 단계마다의 상태를 담아야 합니다. 규칙 사이의 제약도 들어옵니다. mutex group은 규칙 조합 전체를 두고 하는 진술이기 때문입니다. 누적도 들어옵니다. 세 규칙이 같은 fact에서 각각 몇 퍼센트씩 깎아 낸다면, 진짜 질문은 그 합성이 극단에서 어디까지 갈 수 있는가입니다.

물어야 할 질문도 달라집니다. "이 principal이 접근 권한을 얻는 경우가 있는가" 자리에 이런 질문들이 들어섭니다.

• 도달 불가능한 규칙. 우선순위상 위에 있는 모든 것을 감안했을 때, 이 규칙의 조건이 참이 되는 입력이 존재하는지.
• 충돌. 두 규칙이 함께 발동해서 같은 fact에 서로 다른 값을 쓰는 입력이 있는지.
• 공백. 아무 규칙도 발동하지 않아 fact가 끝내 설정되지 않는 입력 영역이 있는지.
• 폭주하는 합성. 겹쳐 쌓인 변경이 값을 아무도 의도하지 않은 경계 너머로 밀어내는 입력이 있는지.

넷 다 가능한 모든 입력에 관한 주장입니다. solver는 답할 수 있고 테스트 스위트는 답할 수 없는 질문이 정확히 이 부류입니다. 입력을 표본으로 뽑는 방식이 왜 구조적으로 이 질문을 닫지 못하는지는 같은 논지의 나머지 절반입니다.

LexQ가 뒤따라가는 쪽입니다

포지셔닝을 꺼내기 전에 먼저 기록해 둡니다. formal verification에서 LexQ는 뒤처져 있습니다. Cedar는 그걸 제품으로 만들었고, LexQ는 그런 종류의 무엇도 제품으로 만들지 않았습니다. 검증된 권한 정책이 지금 검토 중인 요구사항이라면 답은 Cedar입니다. 말을 돌려 문단 하나를 버는 것보다 이렇게 적는 편이 낫습니다.

동시에 참인 사실이 하나 더 있습니다. Cedar가 authorization에서 해낸 그 이동을, 비즈니스 결정 쪽에서는 아직 아무도 하지 않았습니다. 제가 확인한 상용 룰 엔진 중에 규칙 집합 전체를 놓고 formal verification을 제공하는 제품은 없었고, 약한 변형조차 찾지 못했습니다. 시장을 전수 조사했다고까지는 쓰지 않겠습니다. 팀들이 실제로 돌리는 엔진 비교는 호스팅 방식과 운영 부담과 비용의 비교입니다. 무엇을 증명할 수 있는지로 비교되는 엔진은 없습니다. 비교할 대상 자체가 없기 때문입니다.

그래서 위치는 깔끔하게 갈립니다. 기술에서 LexQ는 follower입니다. 도메인에서 그 자리는 아직 비어 있습니다.

Cedar verifies who can access what. LexQ verifies what decision will be made.

두 번째 문장의 시제가 벌어 놓지 않은 값을 하게 두지는 않겠습니다. 이 문장은 두 문제가 무엇인지를 말할 뿐, 두 제품이 오늘 무엇을 하는지를 말하지 않습니다. LexQ 안에 검증 엔진은 없습니다. 이 절에 적힌 어떤 것도 어디서든 돌아가고 있지 않습니다. 이 작업의 이름은 LexQ Verify이고, 지금 그 이름 아래 존재하는 건 문제 정의와 설계 방향, 그리고 이 글입니다.

설계 방향까지는 적습니다. 모양 없는 이름은 마케팅에 지나지 않으니까요. LexQ 규칙 조건을 Z3 SMT solver의 1차 논리 포뮬러로 변환하는 컴파일러를 만들고, 입력 공간 전체를 놓고 충돌과 공백과 도달 불가능 영역을 solver에게 묻는 것입니다. 결과물은 대략 이런 모양을 생각하고 있습니다. 인터페이스의 스케치이지 인터페이스의 스크린샷이 아닙니다.

✅ No unreachable rules
⚠️  2 potential conflicts:
   "vip-discount" ∧ "loyalty-bonus"
   → Resolved by mutex group "promo-exclusive"
❌ 1 gap:
   tier=STANDARD, cartTotal < 5000 is uncovered

왜 아직 아무도 결정 규칙에 이걸 만들지 않았을까요? 아이디어에 감춰진 구석은 없습니다. 걸리는 쪽은 구현입니다. SMT solver를 실무에서 다뤄 본 엔지니어가 드물고, 규칙 조건 DSL에서 SMT 포뮬러로 내려가는 컴파일러 설계는 기능 티켓이 아니라 학술 수준의 난이도입니다. 설계 스케치가 제품 행세를 하게 두느니 그 난이도를 그대로 적는 편이 낫습니다.

오늘 LexQ에 있는 것과 없는 것

선을 한 문단으로 긋습니다. 여기까지 읽은 내용을 믿어도 되는지가 이 문단에서 갈리기 때문입니다. LexQ는 무슨 일이 일어났는지, 그리고 무슨 일이 일어났을지는 말할 수 있습니다. 무슨 일이 일어날 수 있는지는 말하지 못합니다.

선의 앞쪽은 전부 지금 존재하고 돌아갑니다. 변경 영향 시뮬레이션(Impact Simulation)은 규칙 버전을 실제 과거 운영 트래픽에 다시 돌려 그때 어떤 결과가 나왔을지 보여줍니다. 의사결정 재실행(Decision Replay)은 과거의 특정 결정 하나를 다른 버전으로 다시 돌리고 결과를 나란히 비교합니다. 답을 바꾼 규칙이 화면에 그대로 보입니다. 추측할 자리가 없습니다. 모든 실행은 트레이스를 답니다. 어떤 규칙이, 어떤 입력에서, 어느 버전으로 발동했고 나머지는 왜 발동하지 않았는지가 거기 담깁니다. 규칙별 지연 시간 프로파일러는 평가 시간이 어디로 가는지 보여줍니다. 버전은 관리되고 되돌릴 수 있으며, 모든 결정은 불변 감사 로그에 남습니다. 배포 전에 실제 트래픽으로 변경을 확인하는 일과 사후에 어느 규칙이 그 결과를 만들었는지 증명하는 일은 각각 한 편씩 따로 있습니다.

전부 경험적입니다. 하나하나가 실제로 발생한 입력을 놓고 답합니다.

formal verification이 답하는 질문은 부류가 다릅니다. 가능한 모든 입력, 지금까지의 트래픽이 한 번도 만들어 낸 적 없는 입력까지 포함한 질문입니다. 어떤 고객도 아직 밟지 않은 규칙 공백은 시뮬레이션에 구조적으로 보이지 않습니다. 시뮬레이션은 일어난 일만 다시 돌릴 수 있으니까요. 그래서 시뮬레이션을 검증이라고 부르지 않고, 앞으로도 그렇게 부를 생각이 없습니다. 테스트는 증거를 만듭니다. 증명은 다른 물건입니다. LexQ에는 앞의 것이 있고, 앞의 것만 있습니다.

이게 전부 필요 없는 경우

결정 규칙의 formal verification이 모두에게 필요한 건 아니고, LexQ도 마찬가지입니다.

• 규칙 집합이 작고 안정적입니다. 1년째 그대로인 규칙 여섯 개에 solver는 필요 없습니다. 읽으면 됩니다. 그 규모에서는 읽는 것이 증명 절차입니다.
• 실제 문제가 접근 제어입니다. 누가 어떤 리소스에 무엇을 할 수 있는지가 질문이라면 그건 boolean 정책 문제이고, 그 문제만 놓고 만들어진 성숙한 도구가 따로 있습니다. 의사결정 운영 플랫폼보다 Cedar나 OPA가 낫습니다.
• 규칙이 구조적으로 겹칠 수 없습니다. 정확히 한 행만 매칭되는 조회 테이블 하나에는 찾아낼 충돌이 없고, 테이블이 이미 보여주지 않는 공백도 없습니다.
• 아무도 이유를 묻지 않습니다. 시스템이 내린 결정이 분쟁 대상이 되지도, 감사받지도, 몇 달 뒤에 복원되지도 않는다면, 결정을 둘러싼 라이프사이클 전체가 쓰지 않을 장치입니다.

그리고 이 글에서 가장 중요한 항목. 오늘 LexQ Verify가 필요한 사람은 없습니다. 존재하지 않기 때문입니다. formal verification이 지금 검토 중인 실제 요구사항이라면 LexQ는 그 요구를 충족하지 못합니다. 이렇게 적는 대가는 블로그 글 한 줄입니다. 적지 않는 대가는 그보다 훨씬 큽니다.

LexQ는 의사결정 운영 플랫폼입니다. 비즈니스 결정을 애플리케이션 코드 밖의 버전 관리되는 규칙으로 두고, 배포 전에 실제 운영 트래픽에 돌려 확인하고, 배포 후에는 전체 트레이스를 남깁니다.

발표할 기능이 생기기 전에 이 글을 쓰는 이유는, 누가 답하게 되든 이 질문에는 이름이 필요하기 때문입니다. Cedar 팀은 정책 언어의 formal verification이 실현 가능하고 제품화할 값어치가 있다는 걸 보여줬고, 접근 권한에서 보여줬습니다. 가격을 정하고 이체를 통과시키고 청구를 승인하고 기능을 여는 결정은 그보다 크고 지저분하며, 비교하자면 아직 아무도 들여다보지 않았습니다. Cedar는 접근 권한 쪽 질문에 답했습니다. 비즈니스 결정 쪽은 여전히 열려 있고, 아무도 이름 붙이지 않은 질문은 더 오래 열려 있습니다.

→ 오늘 LexQ가 무엇을 하는지부터 확인해보세요. lexq.io에서 무료로 시작하기