실용적인 일차 논리 시제 요구사항의 런타임 강제 구현

런타임 강제기(Runtime enforcers)는 시스템의 동작을 관찰하고 제어하여 시스템이 항상 요구사항을 준수하도록 합니다. 많은 자연스러운 요구사항은 시스템의 현재 동작에 대한 제한만을 공식화하는 것이 아니라, 미래 동작에 대한 의무를 부과하기도 합니다. 예를 들어, 에이전트 보안(agentic security)은 실행 중에 수집된 개인 데이터가 특정 마감일까지 삭제되어야 한다고 요구할 수 있습니다. 끊임없이 성장하는 규정 준수 환경에서 실제 시스템은 수백 가지의 이러한 요구사항을 가질 수 있습니다. 하지만 복잡한 정책을 지원하는 기존의 강제 메커니즘은 프로덕션 소프트웨어에 너무 느린 경우가 많습니다. 대신 개발자들은 비시제적 접근 제어 메커니즘(non-temporal access control mechanisms)과 임시적인 계측(ad-hoc instrumentation)에 의존할 수 있지만, 이는 요구사항의 복잡도에 따라 성능이 저하됩니다. 이 문제를 해결하기 위해, 우리는 복잡한 시제 요구사항을 강제하는 효율적인 알고리즘과 도구를 소개하고 그 성능을 입증합니다. 구체적으로, 우리는 풍부한 실용적 요구사항(의무 포함)을 지원하면서도 낮은 런타임 복잡도로 강제할 수 있는 Metric First-Order Temporal Logic (MFOTL)의 한 조각을 식별했습니다. 그런 다음 이 조각에 대한 강제 알고리즘을 설계하고, 이를 EnfFlash라는 새로운 도구에 구현하여 표준 벤치마크에서 이전 최신 기술인 EnfGuard보다 최대 44배 낮은 지연 시간으로 요구사항을 강제하며, LLM 에이전트의 보안 정책에서는 최대 세 자릿수(three orders of magnitude) 낮은 성능을 보여줍니다. 이러한 성능은 요구사항을 효율적으로 해석하는 명령형 프로그램(imperative programs)으로 컴파일함으로써 달성됩니다. 우리는 EnfFlash를 독립적으로, 기존 벤치마크에서, 그리고 웹 애플리케이션의 강제 백엔드로 통합하여 평가합니다. 우리는 소셜 네트워크에서 GDPR을 명시하는 상당한 길이의 400줄 MFOTL 공식을 적용하면서 페이지 보기당 15ms 미만을 추가할 수 있음을 입증했으며, 이는 대부분의 대화형 및 실시간 애플리케이션에 충분합니다.