안전 모드

안전 모드 (Safe Mode)

소개

안전 모드(safe mode)는 캡처 검사의 확장으로, 프로그램이 추적된 역량이 잊혀질 수 없도록 보장하는 역량-안전 언어 부분집합으로 작성되었음을 강제해요.

출처: Scala 3 Reference

본문

전체 Scala 3에는 타입 캐스트나 다른 안전하지 않은 기능 같은, 역량 안전성과 호환되지 않는 요소들이 있어요. 이것들은 어떤 상황에서는 필수적인 탈출구예요. 하지만 주의해서 사용해야 하고, 리뷰를 통과하지 않은 에이전트 생성 코드나 다른 신뢰할 수 없는 코드에서는 사용할 수 없어야 해요.

이 두 사용 모드를 구분하기 위해, 커맨드 라인 옵션이나 언어 import로 지정할 수 있는 안전한 언어 부분집합이 있어요.

import language.experimental.safe

에이전트형 도구는 에이전트 생성 코드의 모든 컴파일을 이 언어 import를 사용해 안전 모드로 컴파일되게 하는 것이 이치에 맞아요. 안전 모드는 다음 제한들을 부과해요.

검사되지 않은 타입 캐스트나 패턴 매치는 없음.
caps.unsafe 모듈의 기능 사용 없음.
@unchecked 어노테이션과 그 변형의 사용 없음.
런타임 리플렉션에 대한 접근 없음.
모든 변경 효과 추적을 포함해 캡처 검사를 켜고 컴파일.
안전하게 구현된 전역 객체에만 접근 가능.

안전 모드를 사용하는 프로젝트 하나가 TACIT이에요. TACIT은 AI 에이전트를 위한 프레임워크로, 에이전트가 제출한 Scala 3 코드가 타이핑된 역량 API를 통해 실행되기 전에 캡처 검사를 켠 안전 모드에서 검증되고 타입 검사돼요.

검사되지 않은 캐스트나 패턴 매치를 금지해야 하는데, 그것들이 보존된 역량을 "잊어버릴" 수 있기 때문이에요(위 항목 1). caps.unsafe 모듈의 기능(2), @unchecked... 어노테이션의 사용(3), 런타임 리플렉션의 사용(4)에도 같은 이유가 적용돼요. 모든 역량이 타입에 추적되도록 해야 하는데, 특히 순수 함수에서 보존된 역량이 없음을 보장하기 위해서예요(5). 마지막으로 라이브러리 호출을 통한 추적되지 않은 효과의 도입을 막아야 해요. 그래서 라이브러리 모듈은 그것도 안전하게 구현된 경우에만 접근할 수 있어요(6).

안전한 라이브러리 모듈을 구현하는 한 가지 방법은 안전 모드 아래에서 컴파일하는 거예요. 하지만 부작용이 관찰되지 않는 한 일부 안전하지 않은 언어 기능을 허용하는 라이브러리 모듈도 허용해야 해요. 예를 들어 라이브러리 모듈은 함수 결과를 위한 캐시를 구현할 수 있는데, caps.unsafe 모듈에서 오는 @untrackedCaptures 어노테이션으로 표시해 추적되지 않은 변경 가능한 변수를 사용해요. 보통 그런 접근은 안전 모드에서 금지되지만, 다른 수단으로 모듈이 안전하다는 것을 검증할 수 있다면 허용될 수 있어요. 캐시의 구체적인 경우에는, 변수가 이전 함수 호출의 결과만 담고 있고 호출된 함수가 참조 투명(referentially transparent)함을 검증해야 해요. 그러한 검증은 수동으로 비공식적이거나 공식적으로, 또는 기계 지원 정형 증명으로 수행될 수 있어요. 검증이 끝나면 라이브러리 모듈을 안전한 코드가 사용할 수 있게 만들 수 있어요.

이 기법은 caps 모듈에서 사용 가능한 새 @assumeSafe 어노테이션으로 지원돼요. 이 어노테이션이 붙은 모듈은 에이전트 생성 코드에서 호출 가능한 것으로 가정돼요. @assumeSafe는 safe가 뜻하는 제한들을 전혀 가지지 않아요. 대신 모듈이 실제로 안전함을 검증하는 것이 프로그래머의 의무예요.

다음 예시들은 그러한 컴포넌트가 어떻게 구현될 수 있는지 보여줘요. 그것들은 스스로 안전 모드에서 컴파일되지 않아요.

예를 들어 함수 결과 캐싱은 이렇게 구현될 수 있어요.

import language.experimental.captureChecking
import caps.*
import caps.unsafe.untrackedCaptures
import caps.assumeSafe
import scala.collection.mutable.HashMap

@assumeSafe
class Memoized[A, B](f: A -> B) {

  @untrackedCaptures   // allowed since we are not in safe mode
  private val cached = HashMap[A, B]()

  def apply(x: A) = cached.getOrElseUpdate(x, f(x))
}

또는, 보내기 전에 사용자에게 확인을 요청하는 이메일 함수의 개요가 있어요. 여기서는 Mailer 객체가 안전하지도 않고 안전하다고 가정되지도 않는다고 가정해요. 에이전트는 CheckedMailer를 통해서는 여전히 이메일을 보낼 수 있지만, 사용자 확인 후에만 가능해요. 이 구현은 스스로 안전 모드에서 컴파일되지 않아요.

import language.experimental.captureChecking
import caps.*
import language.experimental.captureChecking
import caps.*
case class Email(value: String)

def userPrompt(msg: String): Boolean = true

object Mailer:
  def send(email: Email): Unit = ()
import caps.assumeSafe

@assumeSafe
object CheckedMailer {

  def sendMail(email: Email) =
    if userPrompt(s"OK to send email?\n\n$email") then
      Mailer.send(email) // allowed even if Mailer is not @assumeSafe
                         // since we are not in safe mode
}

caps에는 @assumeSafe의 쌍대(dual)로 볼 수 있는 @rejectSafe 어노테이션도 있어요. 그것은 안전하다고 가정된 컴포넌트의 선택된 멤버를 안전 모드에서 접근 불가능하게 만들어요.

안전 모드는 표준 라이브러리의 부분집합을 사용 가능하게 하는데, 그것은 안전하다고 가정돼요. 이 부분집합은 현재 dotty.tools.dotc.cc.SafeRefs 모듈에서 컴파일러 자체가 정의해요. 그것은 전역 print 함수, java.lang 클래스의 숫자 클래스, 그리고 Enum, String, Object를 제외한 scala 패키지 전체를 포함해요. 또한 java.lang.Class는 포함하지만, 런타임 리플렉션을 구현하는 그 모든 멤버 메서드에 대한 접근은 거부해요. 허용되는 부분집합은 안전 모드에 대한 경험이 더 쌓임에 따라 시간이 지나며 진화할 것으로 기대돼요.

주목할 만한 한 측면은, 라이브러리 호출에 대한 제한이 전역 스코프의 클래스와 객체에만 적용된다는 거예요. 신뢰할 수 없는 코드에 파라미터로 전달되는 역량은 안전하든 안전하지 않든 어떤 모듈에서든 올 수 있어요. 여기서는 API 설계자가 이 역량들에서 적절한 기능만 노출하는 것이 그 작업이에요.

제어 효과 (Control Effects)

안전 모드가 부과하는 제한들은 예외를 던지는 것을 배제하지 않는다는 점을 주목하세요. 예외가 정보를 누출할 수 있는 부작용의 한 형태임에도 그런 경우예요. 이 범위 공백의 이유는 예외가 너무 흔해서 그것들을 모두 정적 타입 시스템에서 제어하는 것이 비현실적이기 때문이에요. 버퍼 오버플로, 스택 오버플로, 0으로 나누기, 메모리 부족 같은 예외에 대해 추가 CanThrow 역량을 요구하는 것은 너무 번거로워요. 이 모든 조건을 역량으로 추적하려고 하기보다, 런타임 보호에 의존해요. 구체적으로 신뢰할 수 없는 코드에 대한 호출은 Try로 감쌀 수 있고, 이것은 던져진 예외를 호출자가 검사할 수 있는 값으로 변환해요. 추가 안전 조치로, 예외 클래스가 순수한 것으로 취급되므로 다른 역량이 예외의 필드로 누출되는 것도 막아져요.

예외와 유사한 다른 제어 효과들도 있어요. 예를 들어 비-지역 반환(non-local return)이나 break, 또는 연속(continuation)의 재개(resumption) 같은 것들이요. 이 효과들도 정보를 누출할 수 있어요. 하지만 Scala 3에서 그것들은 모두 궁극적으로 예외로 표현되므로, Try 런타임 격리(containment) 기법이 그것들에도 적용돼요.