보안 모델을 증명해도 구현 전체가 안전하다는 결론은 나오지 않는다

형식 증명은 정의한 상태, 초기 조건, 전이 규칙과 성질에 대해 결론을 줍니다. 실제 프로그램이 그 모델과 일치하고 모델에 포함된 가정이 충족된다는 연결을 확인하지 않았다면, 증명을 구현 전체의 우회 불가능성으로 넓힐 수 없습니다.

‘모델 안에서 권한 없는 읽기가 도달 불가능하다’와 ‘배포된 제품에 우회가 없다’는 서로 다른 주장입니다. 구현 대응과 모델 밖 경로를 별도 근거로 확인해야 합니다.

증명은 무엇을 전제로 하는가

정형 모델은 현실의 보안 시스템을 전부 복제하지 않습니다. 분석할 상태와 행동을 골라 수학적으로 표현하고, 그 표현 안에서 보안 성질이 유지되는지 확인합니다. 모델이 정확하고 전이 규칙이 빠짐없다는 범위에서 결론은 강력할 수 있습니다. 하지만 그 강도는 모델의 경계를 넘어 자동으로 전달되지 않습니다. 예를 들어 파일 권한 모델에 사용자를 승인·거부 두 상태로만 놓고, 읽기 동작에 권한검사 규칙을 넣었다고 합시다. 모델이 ‘거부 상태에서는 읽기 완료 상태에 도달하지 않는다’를 보일 수는 있어도, 실제 웹 서비스에 존재하는 미리보기 캐시나 관리자 배치 작업은 모델에 없을 수 있습니다.

세 상태로 만든 교육용 접근통제 모델

이 모델의 증명 목표를 ‘S2에 도달했다면 직전 상태가 S1이었다’로 잡으면, 전이 정의를 확인해 성립을 보일 수 있습니다. 이는 모델 내부의 도달 가능성에 대한 주장입니다. 실제 코드에서 모든 읽기 API가 S1과 동등한 검사를 거치는지, 파일 권한 표가 검사 시점에도 최신인지, 실패 시 기본값이 허용이 아닌지까지 표현하지 않았다면 그 부분은 증명되지 않았습니다. 검증된 명제를 그대로 인용하되 모델 가정과 시스템 범위를 함께 밝히는 것이 정확합니다.

모델에서 구현으로 넘어가는 다리

1. 증명한 속성을 한 문장으로 적고 상태·행동·초기조건을 고정합니다.
2. 모델에서 제외한 요소를 찾습니다. 관리자 역할, 백업 복원, 캐시, 오류 처리, 동시 요청, 외부 인증 서비스가 흔한 후보입니다.
3. 각 모델 상태와 전이 규칙이 어떤 코드·구성·운영 절차에 대응하는지 추적합니다.
4. 그 대응을 시험·코드 검토·설계 근거로 확인하고, 값이 불일치할 때 증명 결론이 유지되는지 살핍니다.
5. 조건이 맞지 않거나 검증하지 않은 곳은 한계로 남깁니다. 모델 바깥의 위험은 별도 분석 대상입니다.

예컨대 권한검사 뒤 역할이 바뀔 수 있는 동시 요청을 모델이 허용하지 않는데 실제 서비스는 세션의 역할 정보를 검사와 파일 반환 사이에서 다시 읽는다고 합시다. 모델과 코드의 순서가 다르면 증명된 성질을 코드에 적용할 수 있는지부터 다시 확인해야 합니다. 반대로 구현이 모델보다 더 많은 검사를 한다고 해서 모든 속성이 자동으로 안전해지는 것도 아닙니다. 검사 오류, 입력 정규화 차이, 설정 불일치 등 다른 문제는 여전히 남을 수 있습니다. NIST SP 800-160 Vol. 1 Rev. 1은 시스템 생애주기의 요구·설계·구현·검증을 연결해 보안 근거를 세우는 관점을 제공합니다. NIST CSRC의 assurance case 정의도 주장뿐 아니라 논증·근거·명시적 가정이 연결되어야 한다고 설명합니다.

회상 연습: 증명의 경계를 말합니다

교육용 문제입니다. 모델에는 단일 읽기 API만 있고, 권한이 없는 역할에서 파일 내용을 반환하는 전이가 없음을 증명했습니다. 실제 서비스에 별도 다운로드 API와 미리보기 캐시가 있다면, 이 증명만으로 두 경로도 우회할 수 없다고 결론 내려도 될까요?

아닙니다. 증명은 모델에 정의된 경로와 조건에 대한 결론입니다. 다운로드와 캐시가 모델에 포함됐는지, 코드와 정책이 모델에 대응하는지 확인해야 합니다. 정답을 쓸 때 ‘이 모델의 단일 읽기 전이에서는 권한 없는 반환이 불가능하다’처럼 경계를 유지하면 됩니다.