본 논문은 상호 불신하는 C 프로그램 구획을 위한 공식적으로 안전한 컴파일러 SECOMP를 소개한다. SECOMP는 CompCert 컴파일러를 확장하여 구획화된 프로그램의 안전성을 보장하며, 정의되지 않은 동작의 영향을 해당 구획으로 제한한다.
