Soundness of Programming Languages (Korean)

Programming Language 차원의 Soundness 와 Completeness

• Programming 언어의 Soundness 는 언어의 Type System 의 안정성과 신뢰성을 나타내는 개념입니다.

• 즉, 언어의 Type System 이 Program 의 Type 관련 오류를 모두 잡아낼 수 있다면, 그 언어는 “Sound 하다” 라고 합니다.

• 이는 Programming Language 가 제공하는 Satety 와 Correctness 의 척도로 볼 수 있으며, 프로그래머가 Runtime Error 없이 더 안전한 코드를 작성할 수 있게 돕습니다.

Soundness 의 의미

• Type Safety (타입 안전성)

  • Program 이 실행될 때 Type Error 가 발생하지 않음을 보장함.

  • 예를 들어, 정수형 변수에 문자열을 할당하는 등의 오류를 Compile 시간에 감지하여 Runtime 오류를 예방합니다.

• Predictability (예측 가능성)

  • Program 의 동작이 Type System 에 의해 명확하게 정의되어 있어, 개발자가 코드의 동작을 예측하기 쉽습니다.

• Reliability (신뢰성)

  • Type System 의 강력한 검증으로 인해 프로그램이 더 안정적으로 실행됩니다. Type 오류로 인한 예기치 않은 실패를 줄일 수 있습니다.

Soundness 의 중요성

• Soundness 는 특히 큰 규모의 소프트웨어 프로젝트나, 안전성이 중요한 시스템을 개발할 때 중요한 역할을 함.

• Type System 의 엄격한 검증을 통해 개발 초기 단계에서 오류를 발견하고 수정할 수 있으므로, 유지 보수 비용을 절감하고 소프트웨어의 전반적인 품질을 향상 시킬 수 있음.

Soundness 와 Completeness

• Soundness 는 종종 Completeness 와 대비됨.

• 언어가 Complete 하다는 것은 그 Type System 이 Program 의 모든 유효한 동작을 허용한다는 의미.

• 하지만, 언어가 “Complete 하다” 해서 반드시 Sound 한 것은 아닙니다.

• 이상적으로는 Type System 이 Sound 하면서도 충분히 유연하여 다양한 Programming Pattern 을 지원하는 것이 좋다.

Soundness 의 한계

• 모든 Type Error 를 Compile 시간에 검출하는 것은 현실적으로 어렵거나 불가능할 수 있음.

• 특히 Dynamic Type 언어(i.e Ruby, Python, Javascript 등) 에서는 Runtime 에 Type 을 결정하므로, Compile Time 에 모든 Type 오류를 잡아내는 것이 어려움.

• 따라서, Soundness 는 Programming Language 가 추구해야 할 목표 중 하나 이지만, 완벽하게 달성하기 어려운 속성임.

• Programming Language 의 선택이나 설계 시, Soundness 는 중요한 고려 사항 중 하나 입니다.

• 언어의 Type System 이 얼마나 강력한지, 그리고 어떤 유형의 오류를 Compile Time 에 잡아낼 수 있는지는 프로젝트의 성공과 안정성에 직접적인 영향을 미칩니다.

The benefits of Soundness

• Compile time 에 Type 관련 버그들을 발견할 수 있습니다.

  • Sound 한 Type System 은 Type 들에 대해서 모호(Ambiguous) 하지 않게 강제할 수 있습니다.

  • 그래서 Runtime 시에는 발견하기 힘든 Type 관련 버그들을 Compile Time 에 발견할 수 있습니다.

• Code 의 Readability 를 향상 시킨다.

  • 어떠한 Value 가 특정한 Type 을 가지기 때문에 우리는 Value 만 신경 쓰면 되기 때문에 Code 를 읽기가 쉬워집니다.

  • Sound 한 Dart 언어의 Type 은 거짓을 말하지 않습니다.

• 유지 보수하기 쉬운 코드를 작성할 수 있다.

  • Sound 한 Type System 으로 Code 한 줄을 고친다고 하면, Type System 은 Code 의 다른 부분에서 Break 할 수도 있다고 경고를 줄 수 있습니다.

• 좋은 AOT(Ahead of Time) Compile 을 할 수 있다.

  • Strong Type System 에서 미리 Type 검사를 수행하는 AOT Compile 은 Runtime 에서 발생할 수 있는 타입 불일치와 같은 문제를 사전에 방지합니다. 따라서 Strong Type System 과 AOT Compile 을 함께 사용할 경우, Type Safety 와 Execution Performance 모두를 향상 시킬 수 있습니다.

  • AOT Compile 은 Source Code 를 실행하기 전에 미리 Machine Language 또는 Intermediate Code로 컴파일하는 방식을 말합니다. 이는 JIT(Just-In-Time) Compile 과 달리, Runtime 에 Compile 하지 않고 프로그램을 실행하기 전 Compile 을 완료하기 때문에 실행 속도가 빠르고 초기 성능 최적화에 유리합니다. AOT Compile 은 미리 Compile 된 Machine Language 를 실행하므로, Memory 나 CPU Resource 사용이 더 효율적일 수 있습니다.

• 보다 깔끔한 Javascript 를 작성할 수 있다.

  • Web application 에서 strong mode 로 작동하는 제한된 typing 은 dartdevc 가 보다 깔끔하고 compact 한 Javascript 를 생성할 수 있게 해준다.

Static Analyzer (Code 분석기) 차원의 Soundness 와 Completeness

Soundness

• 분석기가 식별한 모든 문제가 실제로 코드 내에 존재하는 문제임을 보장

• Sound 분석에서는 False Positive (잘못된 경고) 은 있을 수 있어도 False Negative (실제 오류를 놓치는 경우) 은 없어야 합니다.

  • False Positive

    • 분석기는 오류가 있음 (Positive) 이라고 말하는데, 사람이 확인해 보니 오류가 아님 (False)

  • False Negative

    • 분석기는 오류가 없음 (Negative) 라고 말하는데, 사람이 확인해 보니 오류가 있음 (False)

• 보다 더 Sound 한 분석을 하려고 할 때, 일부 유효한 문제를 놓칠 수 있는 False Negative (실제 오류를 놓치는 경우) 의 가능성이 증가

• Statements 가 Model 에서 증명한 것들이 정말로 True 이면, 증명 시스템은 “Sound 하다” 고 한다.

  • Statements

    • Model 에 대해서 증명할 수 있는 속성들

  • Model

    • 어떤 Domain 에 있는 집합 (수학적인 구조)

Completeness

• Code 분석기가 가능한 모든 실행 경로와 프로그램의 모든 가능한 상태를 분석하여, 주어진 유형의 오류나 버그를 놓치지 않고 정확하게 식별할 수 있는 능력을 의미

• 보다 더 Complete 한 분석을 하려고 할 때, 분석의 복잡성과 수행 시간이 증가하며, 이는 False Positive (잘못된 경고) 의 수를 증가 시킬 수 있습니다.

• Model 에 있는 어떠한 True statement 도 증명할 수 있다면, 증명 시스템은 “Complete” 하다 고 한다.

• 그래서 분석기가 특정 Program 을 “Sound(accepts only true programs) 하고 Complete(rejects all false programs) 하다” 라고 판단 한다면, 그 Program은 'True' 하고 'Not False' 하다 라고 말할 수 있음.

  • 이것은 Turing Machine(분석기)이 모든 입력에 대해 중지 하거나 결정한다는 것을 의미.

    Turing Machine

    • 이론적인 컴퓨팅 장치입니다. 영국의 수학자 Alan Turing 이 개념을 처음으
      로 제안.

    • Tape, Head, State, Transition 함수로 구성되어 있다.

      1. Turing Machine 은 초기 State 로 시작

      2. 현재 State 와 현재 읽은 기호를 확인하고 Transition 함수를 사용하여 다음 동작을 결정

      3. Transition 함수에 따라 Turing Machine 은 다음 상태로 이동하고, Tape 의 내용을 변경하고, Head 를 왼쪽 또는 오른쪽으로 이동합니다.

      4. 이러한 과정을 반복하면서 Turing Machine 은 입력 데이터를 처리하고 원하는 작업을 수행합니다.

    • Turing Machine 은 이론적으로 모든 계산을 수행할 수 있는 것으로 알려져 있습니다.

예제로 살펴보는 Soundness and Completeness

• Tool A (왼쪽 상단의 작은 원)

  • Sound and Not Complete

  • p1, p2 가 에러가 없다는 것을 증명

• Tool B (왼쪽의 원)

  • Not Sound and Not Complete

  • p3, p4 는 에러가 없다는 것을 증명하지만, p5 는 에러가 없다는 것을 증명하지 못함

  • p6 는 Tool B 가 검증을 할 수 없는 영역에 위치함

• Tool C (5각형)

  • Complete

  • 모든 프로그램 p1, p2, p3, p4, p5, p6 에 대해서 검증할 수 있음

• 예제에서 살펴보는 False Alarm

  • Tool A 의 관점에서 보면 p3, p4 는 False (False Positive) Alarm 에 해당함

    • 왜냐하면 Tool B 에서는 에러가 없다고 증명했기 때문

  • 대부분의 분석기 디자이너들은 False Negative Alarm 을 줄이기 위해서 분석기를 Sound 하지 않게 만들기도 한다.

    • False Negative Alarm 은 몇몇 상황에서 분석기 사용자 입장에서 중요한 문제를 발견할 수 없게 하기 때문이다.

    • 그래서 분석기는 확실하게 오류(True Positive) 라고 할 수 있는 것 만을 Alarm 으로 알려주는 것이 좋은 분석기라고 하기도 한다.

  • 분석기 입장에서 해당 Program 에 Error 가 있다고 알려주는 모든 것들이 False (False Positive) Alarm 이 아닌 것을 “Complete 하다” 라고 한다.

• 그래서 분석기를 너무 Sound 하게 하지도 않고, 너무 Complete 하게 하지 않도록 잘 조율하는 것이 Static Analyzer 입장에서는 중요함.

Type Safety

Luca Cardelli and Type Safety

• Program 이 Safe 하다는 것은 미처리 오류 (Untrapped Error) 를 발생 시키지 않는 것을 의미함.

• 모든 가능한 실행 오류의 Subset 을 Forbidden Error 로 정의함.

  • 이것은 미처리 오류와 처리된 오류 (Trapped Error) 의 Subset 을 가리킴

• Well-Behaved 프로그램은 Forbidden Error 가 발생하지 않는 것을 의미

• 그러므로 Well-Behaved Program 은 “Safe 하다” 고 할 수 있음

• Program 이 Strongly Checked (강력하게 검사된) 다는 것은 모든 합법적인 Program 이 Well-Behaved (잘 작동하는) 이라는 것을 의미합니다.

• Strongly Checked Program 은 아래와 같은 속성을 가집니다.

  • 미처리 오류가 발생하지 않는다. (Safety)

  • 금지된 오류에 속하는 미처리 된 오류가 발생하지 않음

  • 다른 처리된 에러가 발생할 수 있음

Benjamin C. Pierce and Type Safety

• Lambda Calculus 의 맥락에서, Stuck State 를 아래와 같이 Formalize 할 수 있음

  • 만약 Closed Term 이 Normal Form 을 갖고 있지만, 값 (Value) 이 아니라면, 해당 Term 은 Stuck (멈춘 상태) 로 말할 수 있다.

    • Normal Form (정규 형태)

      • 주어진 Expression 이 더 이상 평가될 수 없는 상태를 나타냄

      • Expression 이 더 이상 단순화되거나 계산되지 않고 최종 결과로 평가 되었음을 의미

    • Closed Term ( 닫힌 항)

      • 자유 변수가 없는 표현식(Expression) 을 의미

      • 모든 Variable 이 해당 Expression 내에서 바인딩(Bound)되어 있어, 외부 환경에 의존하지 않고 독립적으로 평가될 수 있는 식을 말합니다.

    • Values

      • 평가의 최종 결과가 될 수 있는 모든 가능한 Term

    • Normal Form

      • Term 't' 가 어떤 Evaluation 규칙도 적용되지 않은 상태일 때

• 정리를 통해 Well-Typed 의 정의를 아래와 같이 제안

  • Progress

    • Well-Typed 된 Term 은 멈춘 상태가 아닙니다.

  • Preservation

    • Well-Typed 된 Term 이 Evaluation 단계를 거치면 결과로 나온 Term 도 “Well-Typed” 라고 할 수 있음

Type Safety Introduction in easy way

Type Safety

• Type Safety 의 의미를 직관적으로 풀어 써보면 "Well-Typed Program 은 잘못되어질 수 없다" 를 의미

• 이 표현은 1978년 Robin Miller의 논문 'A Theory of Type Polymorphism in Programming' 에서 만들어짐

잘못되어지는 것

• Programming Language 는 개발자가 작성하도록 허용된 Syntax 와 작성된 Program 이 가지는 의미인 Semantics 로 정의된다.

• 모든 Programming 언어는 Syntatic 하게는 옳지만, Semantics 가 옳지 않은 문제를 겪는다.

• Chomsky 고전의 문장인 “Colorless green ideals sleep furiously”는 문법적으로는 아무런 문제가 없지만, 이는 아무런 의미가 없다.

• OCaml 언어로 예를 들어, 1 + "foo"; 는 프로그램의 Semantic 를 따져보았을 때 아무런 의미가 없다.

• 또 다른 예시는 C 언어로 { char buf[4]; buf[4] = ‘x’ } 를 들 수 있다.

  • 이것 또한 버퍼의 범위 밖의 인덱스 4에 쓰기 접근을 하기 때문에 언어의 정의는 이러한 행동을 Undefined behavior(의미없는 것)으로 분류한다.

  • 이러한 의미없는 프로그램을 우리가 실행하게 된다면, 프로그램은 잘못된 행동을 발생시킴.

Well-typed

• Type-Safe 한 언어의 세계에서는, 언어의 Type System 이 특정 방법으로 "옳은"(잘못되어지지 않는) Program 만을 받아들인다.

• 특히, Type System 이 받아들인 프로그램을 “Well-Typed” 이라 하고, Type-Safety 는 이러한 프로그램이 절대로 잘못되어지지 않음을 보장한다.

• 이를 시각화 하면 아래와 같다.

• 

• Type-Safe 한 언어의 세계에서, Well-Typed 프로그램은 Well-Defined 프로그램의 부분 집합이 된다.

Type Safety of well known programming languages

C/C++

• Not Type-Safe

• C 의 Type System 은 Coding Standard 나 개발자의 일반적인 상식에서 의미 없다고 판단하는 프로그램을 배제 시키지 않는다.(i.e. Buffer 의 Index 를 벗어난 Program)

• 그러므로, C 언어에서는 Well-Typed 된 프로그램도 잘못되어질 수 있다.

• 그리고 사실상 C 언어의 상위 집합인 C++ 언어는 이러한 C 언어의 Type 불완전성을 상속 받았습니다.

Java / C#

• Type-Safe

• 언어의 구현이 Type-Safe 한지 확신하는 것은 꽤 어렵지만,(i.e. 초기 버전 Java 의 Generics 은 Bug 가 많았다.)

• 좀 더 형식화 된 언어의 하나인 Java 는 Type-Safe 하다고 할 수 있다.

• Java 의 Type Safety 의 개념은 C 의 Semantics 에서는 정의되지 않았던 것들이 이들 언어에서는 의미가 주어졌다.

• 예를 들어, C 프로그램에서 Array 의 범위 바깥에 접근하는 행동은 정의되지 않은 것이지만, Java 나 C# 에서는 정의되어 있다.

  • 이 경우, 프로그램이 ArrayBoundsException을 던질 것이다.

Python / Ruby

• Not Type-Safe

• Python 이나 Ruby 는 Dynamically-Typed 된 언어로 구분됨, 그래서 Type 관련 Error 가 Runtime 에 발생할 수 있음.

• 이들은 Type Error 를 알리기 위해 Runtime 에 발생하는 Type Error 에 대해 예외를 던진다.

• Java 가 Array Overflow 에 대해 ArrayBoundsException 를 던지는 것처럼, Ruby 는 String Type 과 Integer Type 에 더하는 연산을 할 때, 예외를 던질 것이다.

• 두 경우 모두, 이러한 프로그램 행동은 언어의 Semantics 에 의해 규정되어있기 때문에 Well-Defined 라고 할 수 있다.

• Java 언어에서, 프로그램 o.m()이 Well-Typed 라면, Type Safety 는 o 가 Method m 에 대해 Argument 를 받지 않는 Object 라는 것을 보장하고, Method 의 호출은 성공할 것이다.

• Ruby 언어에서, Ruby 의 Type System 에 Well-Typed 된 프로그램 o.m() 를 실행한다면, o 가 Method m 을 정의한다는 것을 보장할 수 없으며 호출이 성공할 수도, 예외가 발생할 수도 있다.

• Type Safety 는 단순히 한 가지를 의미하지 않는다. 그것이 보장하는 것은 언어의 Semantics 에 따라 달라지며, 잘못된 행동을 내포할 수도 있다.

  • Java 언어에서, 존재하지 않는 Method 를 호출하는 것은 잘못된 행동이다. (Compile 에 실패할 것이다.)

  • Ruby 언어에서는 존재하지 않는 Method 를 호출하는 것은 잘못된 행동이 아니다. (단순히 예외를 발생시키고 말 것이다.)

Javascript

• Not Type-safe

• 동적 타입 시스템(Dynamic Type System) 을 사용하기 때문

• Compile Time 에 Type 관련 Error 를 포착하는 것이 어렵고, 이는 실행 시간에 Type Error 가 발생할 가능성을 증가

• TypeScript 를 사용하면 Type-Safe 하게 사용할 수 있음 (Static Type System 을 추가)

Go

• 일반적으로 Type-Safe

• 정적 Type 언어로 분류되며, Compile 가 변수와 Expression 의 Type 을 검사하여 Type 관련 Error 를 미리 방지

• 그러나 명시적인 Type Annotation 을 강제하지 않음, Type Inference 를 사용

• 종합적으로, Type Safety 를 중요시하며, 정적 Type 검사를 통해 안정성을 보장하려고 함.

Kotlin

• Type-Safe

• Variable 과 Expression 의 Type 을 Compile Time 에 엄격하게 검사

• Null Safety 를 강조하며, Variable 이 null 값을 가질 수 있는지 여부를 명시적으로 지정

• Static Type Check 을 통해 안정성을 보장

Scala

• Strongly Type-Safe

• Variable 과 Expression 의 Type 을 Compile Time 에 엄격하게 검사

• Type System 은 강력하며, 높은 수준의 추상화와 유연성을 제공하는 동시에, Type Error 로부터 안전성을 보장

• 타입 추론(Type Inference) 기능은 Code 의 가독성과 간결성을 향상 시키면서도 Type 의 정확성을 보장

Rust

• Strongly Type-Safe

• Compile Time 에 모든 Type 을 Check

• 강력한 Type System 과 소유권 모델을 사용하여 Compile Time 에 Memory 안전성(Memory Safety) 을 보장

• 실행 시간에 발생할 수 있는 많은 종류의 Bug 와 안전하지 않은 동작을 방지

• Type System 은 Variable, Function, Expression 등의 Type 을 명시적으로 선언하거나 Compiler 가 Type 을 추론하게 함으로써 작동

• 소유권 시스템은 데이터 경합(Data Race)과 같은 동시성 오류를 Compile Time 에 방지

• Variable 이 여러 소유자를 가질 수 없게 하며, 한 번에 하나의 데이터에 대한 변경 만을 허용하여 안전한 동시성 프로그래밍을 가능하게 함

Benefits of Type-Safe Programming Language

오류 감소

• Type-Safe 한 언어는 Compile Time 에 Type 관련 오류를 감지하고 수정하도록 강제합니다.

• 이는 실행 시간에 발생할 수 있는 오류를 크게 줄여주며, 결과적으로 보다 안정적인 Program 을 만들 수 있도록 도와줍니다.

Code 유지 관리를 용이하게 함

• Type System 은 Code 의 의도를 명확히 하고, 다른 개발자가 Code 를 이해하고 수정하는 데 도움을 줍니다.

• Type 선언과 검사는 Code 의 문서화 역할을 하며, Code Base 가 커지고 복잡해질수록 이점이 더욱 부각됩니다.

Refactoring 의 안전성 증가

• Type 검사를 통해 Refactoring 시 발생할 수 있는 오류를 미리 감지할 수 있습니다.

• Type-Safe 은 Code 변경이 예상치 못한 Side Effect 를 일으키지 않도록 보호하는 안전망 역할을 합니다.

자동화된 도구 지원 향상

• Type 정보는 IDE(통합 개발 환경)와 같은 도구에서 Code 자동 완성, Static Analysis, Refactoring 지원 등 다양한 기능을 제공하는 데 활용됩니다.

• 개발자의 생산성을 크게 향상 시킵니다.

성능 최적화 가능성

• Compiler 는 Type 정보를 사용하여 최적화를 수행할 수 있습니다.

• 예를 들어, Data Type 에 따른 메모리 배치 최적화나, 실행 시 Type Check 를 줄일 수 있는 최적화 등이 있습니다.

보안성 증가

• Type-Safe 은 특정 종류의 보안 취약점을 방지하는 데 도움을 줄 수 있습니다.

• 예를 들어, Buffer Overflow 와 같은 메모리 관련 오류는 Type System 을 통해 효과적으로 관리될 수 있습니다.

• White House urges developers to dump C and C++ (백악관에서 개발자들에게 C, C++ 을 버리고 Rust 와 같은 안전한 Programming Language 를 사용하라고 가이드)

  • US President Joe Biden’s administration wants software developers to use memory-safe programming languages and ditch vulnerable ones like C and C++.

  • Memory-safe programming languages are protected from software bugs and vulnerabilities related to memory access, including buffer overflows, out-of-bounds reads, and memory leaks.

  • The new 19-page report from ONCD gave C and C++ as two examples of programming languages with memory safety vulnerabilities, and it named Rust as an example of a programming language it considers safe.

• Linus Torvalds: Rust will go into Linux 6.1 (리누스 토발즈가 Linux 6.1 에 Rust 로 작성된 Code 가 들어간다고 이야기 함)

요약

• Sound 한 Program 은 여러가지 장점이 있고, 이는 Type System 을 어떻게 설계하는 지에 영향을 많이 받습니다.

• 결국 Type Safety 와 Soundness 는 서로 긴밀한 관계가 있고, Programming Language 를 설계하는 Designer 들은 이를 잘 조율해야 합니다.

• 오늘날 Type Safe 한 Programming Language 들이 각광 받는 이유는 C, C++ 과 같은 Type System 이 Syntax 적으로는 옳지만, Semantic 하게 옳지 않음을 어느 정도 허용하여 발생하는 메모리 관련 오류들이 보안 문제를 야기하고 있기 때문입니다.

• Type Safe 한 Programming Language 들은 생산성, 안정성 측면에서 좋은 점들이 많기 때문에 이러한 특징을 잘 이용하여 적절한 곳에 사용하면 좋습니다.

참고자료

• Type Safety in OCaml Language (Youtube)

• What is soundness in static analysis?

• False Positives in Static Code Analysis

• Type Systems for Programming Languages

• The Type System Every Programmer Should Know

• A Type System From Scratch – Robert Widmann (Youtube)

• Types and Programming Languages (Book)