언어 기반 보안

Language-based security

컴퓨터 과학에서 언어 기반 보안(LBS)은 프로그래밍 언어의 특성을 이용하여 높은 수준에서 응용 프로그램의 보안을 강화하기 위해 사용될 수 있는 일련의 기술이다.LBS는 기존 운영체제 보안이 처리할 수 없는 취약점을 예방할 수 있도록 애플리케이션 차원에서 컴퓨터 보안을 강제하는 것으로 검토되고 있다.

소프트웨어 애플리케이션은 일반적으로 특정 프로그래밍 언어로 지정되고 구현되며, 공격, 결함 및 버그에 취약할 수 있는 애플리케이션 소스 코드가 보호하려면 애플리케이션 수준의 보안이 필요하다. 즉, 프로그래밍 언어와 관련된 애플리케이션 동작을 평가하는 보안.이 영역은 일반적으로 언어 기반 보안으로 알려져 있다.

동기

SCADA와 같은 대형 소프트웨어 시스템의 사용은 전 세계적으로[1] 일어나고 있으며 컴퓨터 시스템은 많은 인프라의 핵심을 이루고 있다.사회는 물, 에너지, 통신, 교통과 같은 기반시설에 크게 의존하고 있으며, 다시 한번 이 모든 것들은 완전히 기능적으로 작동하는 컴퓨터 시스템에 의존하고 있다.컴퓨터 메모리 부족으로 인해 LASC 컴퓨터가 다운되고 수백 편의 비행이 지연된 경우(2014년 4월 30일)와 같이 중요한 시스템이 버그나 소프트웨어의 오류로 인해 고장난 경우 몇 가지 잘 알려진 예가 있다.[2][3]

전통적으로 소프트웨어의 정확한 동작을 제어하기 위해 사용되는 메커니즘은 운영체제 수준에서 구현된다.운영 체제는 메모리 액세스 위반, 스택 오버플로 위반, 액세스 제어 위반 및 기타 많은 기타 가능한 보안 위반을 처리한다.이것은 컴퓨터 시스템의 보안에 있어서 중요한 부분이지만, 보다 구체적인 수준에서 소프트웨어의 행동을 확보함으로써, 훨씬 더 강력한 보안을 달성할 수 있다.컴파일에서 소프트웨어의 많은 속성과 동작이 손실되기 때문에, 기계 코드의 취약성을 검출하는 것은 훨씬 더 어렵다.소스 코드를 평가함으로써, 컴파일 전에, 프로그래밍 언어의 이론과 구현도 고려할 수 있으며, 더 많은 취약점을 발견할 수 있다.

"그러니까 개발자들은 왜 자꾸 똑같은 실수를 저지르는 거지?프로그래머의 기억력에 의존하지 말고 공통의 보안 취약점에 대해 알려진 것을 코드화해 개발 과정에 직접 통합하는 도구를 만드는 데 힘써야 한다고 강조했다.

— D. 에반스와 D.라로셸, 2002년

언어 기반 보안 목표

LBS를 사용함으로써, 소프트웨어의 보안은 사용되는 기술에 따라, 몇 가지 영역에서 증가될 수 있다.버퍼 오버플로 및 불법 정보 흐름의 발생 허용과 같은 일반적인 프로그래밍 오류는 소비자가 사용하는 소프트웨어에서 감지하여 허용하지 않을 수 있다.또한 소프트웨어의 보안 속성에 대한 일부 증거를 소비자에게 제공하여 소비자가 소스 코드를 수신하지 않고도 소프트웨어를 신뢰할 수 있게 하고 오류가 있는지 스스로 확인할 수 있도록 하는 것이 바람직하다.

컴파일러는 소스 코드를 입력으로 받아 기계 판독 가능한 코드로 변환하기 위해 코드에 대해 몇 가지 언어별 작업을 수행한다.어휘 분석, 사전 처리, 구문 분석, 의미 분석, 코드 생성, 코드 최적화는 모두 컴파일러에서 일반적으로 사용되는 작업이다.소스 코드를 분석하고 언어의 이론과 구현을 이용하여 컴파일러는 프로그램의 동작을 보존하면서 하이 레벨 코드를 로우 레벨 코드로 올바르게 번역하려고 시도할 것이다.

인증 컴파일러 설명

자바와 같은 형식 안전 언어로 작성된 프로그램을 컴파일하는 동안, 소스 코드는 컴파일하기 전에 성공적으로 타이핑 검사를 해야 한다.형식 검사에 실패하면 컴파일이 수행되지 않으며, 소스 코드를 수정할 필요가 있다.즉, 올바른 컴파일러를 사용할 경우 성공적으로 타이핑된 소스 프로그램에서 컴파일된 모든 코드가 잘못된 할당 오류를 제거해야 한다.특정 오류로 인해 프로그램이 중단되지 않을 것이라는 보장이 어느 정도 제공되기 때문에 이는 코드 소비자에게 중요한 정보가 될 수 있다.

LBS의 목표는 소프트웨어의 안전 정책에 해당하는 소스 코드에 특정 속성이 존재하는지 확인하는 것이다.컴파일 과정에서 수집된 정보는 해당 프로그램에서 안전성의 증명으로 소비자에게 제공할 수 있는 인증서를 만드는 데 사용할 수 있다.그러한 증거는 소비자가 공급자가 사용하는 컴파일러를 신뢰할 수 있고 소스 코드에 대한 정보인 인증서가 검증될 수 있음을 의미해야 한다.

그림은 인증 컴파일러를 사용하여 낮은 수준의 코드에 대한 인증과 검증이 어떻게 설정될 수 있는지를 보여준다.소프트웨어 공급업체는 소스 코드를 공개하지 않아도 된다는 이점을 얻고 소비자에게는 인증확인 업무가 맡겨져 소스 코드 자체의 평가와 편성에 비해 손쉬운 작업이다.인증서 확인에는 컴파일러와 검증자가 포함된 제한된 신뢰 코드 베이스만 필요하다.

기술

프로그램 분석

주요기사 : 프로그램분석

프로그램 분석의 주요 적용 분야는 프로그램 최적화(재생 시간, 공간 요구 사항, 전력 소비량 등)와 프로그램 정확성(벅지, 보안 취약성 등)이다.프로그램 분석은 컴파일(정적 분석), 런타임(동적 분석) 또는 둘 모두에 적용할 수 있다.언어 기반 보안에서 프로그램 분석은 유형 검사(정적 및 동적), 모니터링, 도색 검사 및 제어 흐름 분석과 같은 몇 가지 유용한 기능을 제공할 수 있다.

정보 흐름 분석

주요 기사:정보 흐름

정보 흐름 분석은 정기적인 접근 제어 메커니즘이 부족한 경우 기밀성과 무결성을 보존하기 위해 프로그램에서 정보 흐름 제어를 분석하는 데 사용되는 도구 집합으로 설명할 수 있다.

"정보에 대한 접근권을 전파권으로부터 분리함으로써, 흐름 모델은 보안 정보 흐름을 규정하는 능력에서 접근 매트릭스 모델을 넘어선다.실질적인 시스템은 모든 보안 요건을 충족시키기 위해 접근과 흐름 제어를 모두 필요로 한다."

— D. 데닝, 1976년

접근 통제는 정보에 대한 접근에 대한 검사를 시행하지만, 그 이후에 무슨 일이 일어날지는 우려하지 않는다.예:시스템에는 앨리스와 밥이라는 두 명의 사용자가 있다.앨리스는 파일 비밀을 가지고 있다.txt는 그녀에 의해서만 읽히고 편집될 수 있으며, 그녀는 이 정보를 혼자 간직하는 것을 선호한다.시스템에는 파일 공개도 존재한다.txt(시스템에 있는 모든 사용자에 대해 자유롭게 읽고 편집할 수 있음)앨리스가 실수로 악의적인 프로그램을 다운로드했다고 가정해보자.이 프로그램은 비밀에 대한 접근 제어 검사를 우회하여 앨리스로 시스템에 접속할 수 있다.그러면 악의적인 프로그램은 비밀의 내용을 복사한다.땡땡이 치고 공공장소에 내놓는다.txt, Bob과 다른 모든 사용자가 읽을 수 있도록 허용.이것은 시스템의 의도된 비밀 유지 정책의 위반에 해당한다.

비간섭

비간섭(non interference)은 보안 등급이 낮은 변수의 입력에 따라 보안 등급이 높은 변수의 정보가 유출되거나 노출되지 않는 프로그램의 속성이다.비간섭을 만족하는 프로그램은 낮은 변수의 동일한 입력을 사용할 때마다 동일한 출력을 생성해야 한다.이것은 입력의 가능한 모든 값을 지탱해야 한다.이는 프로그램의 상위 변수가 실행마다 값이 다르더라도 하위 변수에서는 이를 볼 수 없어야 함을 의미한다.

공격자는 비간섭을 만족시키지 못하는 프로그램을 반복적이고 체계적으로 실행하여 그 동작을 매핑하려고 시도할 수 있다.여러 번 반복하면 더 높은 변수가 노출될 수 있으며, 공격자가 예를 들어 시스템 상태에 대한 중요한 정보를 알 수 있다.

프로그램이 비간섭을 만족하는지 여부는 보안형 시스템의 존재를 가정하여 컴파일 중에 평가할 수 있다.

보안형 시스템

주요 기사:보안형 시스템

보안형 시스템은 소프트웨어 개발자가 코드의 보안 속성을 확인하기 위해 사용할 수 있는 일종의 유형 시스템이다.보안 유형이 있는 언어에서 변수와 표현식의 유형은 애플리케이션의 보안 정책과 관련되며 프로그래머는 유형 선언을 통해 응용 프로그램 보안 정책을 지정할 수 있다.형식은 (접근통제나 능력으로) 인가정책, 정보흐름 보안 등 다양한 종류의 보안정책을 추론하는 데 사용할 수 있다.보안형 시스템은 정식으로 기본 보안 정책과 관련될 수 있으며, 형식 점검하는 모든 프로그램이 의미론적 의미에서 정책을 만족한다면 보안형 시스템은 건전하다.예를 들어 정보 흐름에 대한 보안 유형 시스템은 비간섭을 강제할 수 있으며, 이는 유형 점검이 프로그램에 기밀성 또는 무결성 위반이 있는지 여부를 드러낼 수 있다는 것을 의미한다.

로우 레벨 코드 확보

로우 레벨 코드의 취약성은 프로그램의 추가 동작이 소스 프로그래밍 언어에 의해 정의되지 않는 상태로 프로그램을 이끌 버그나 결함이다.저수준 프로그램의 동작은 컴파일러, 런타임 시스템 또는 운영체제 세부사항에 따라 달라질 것이다.이를 통해 공격자는 프로그램을 정의되지 않은 상태로 유도하고 시스템의 동작을 이용할 수 있다.

보안되지 않은 로우 레벨 코드의 일반적인 악용으로 공격자는 메모리 주소에 무단 읽기 또는 쓰기를 수행할 수 있다.메모리 주소는 무작위일 수도 있고 공격자가 선택할 수도 있다.

안전한 언어 사용

안전한 로우 레벨 코드를 달성하기 위한 접근법은 안전한 하이 레벨 언어를 사용하는 것이다.안전한 언어는 프로그래머의 매뉴얼에 의해 완전히 정의되는 것으로 간주된다.[4]안전한 언어로 구현에 의존하는 행동을 유발할 수 있는 버그는 컴파일 시간에 감지되거나 런타임에 잘 정의된 오류 행동을 유발할 수 있다.Java에서, 범위를 벗어난 어레이에 액세스할 경우 예외가 발생한다.다른 안전한 언어의 예로는 C#, Haskell, Scala가 있다.

안전하지 않은 언어의 방어적 실행

안전하지 않은 언어 런타임 검사를 컴파일하는 동안 소스 수준의 정의되지 않은 동작을 탐지하기 위해 로우 레벨 코드에 추가된다.한 예로 경계 위반을 발견할 때 프로그램을 종료할 수 있는 카나리아 사용이 있다.한계 점검과 같은 런타임 점검을 사용하는 단점은 상당한 성능 오버헤드를 부과한다는 것이다.

실행 불가능한 스택 및/또는 힙을 사용하는 것과 같은 메모리 보호는 추가 런타임 검사로도 볼 수 있다.이것은 많은 현대적인 운영 체제에서 사용된다.

모듈의 격리된 실행

소스코드를 분석해 애플리케이션 데이터에서 민감한 코드를 파악한다는 게 일반적인 생각이다.이 작업이 완료되면 서로 다른 데이터가 분리되어 다른 모듈에 배치된다.각 모듈이 포함된 민감한 정보에 대한 완전한 제어를 가지고 있다고 가정할 때, 모듈에서 언제 어떻게 나가야 하는지 지정할 수 있다.키가 암호화되지 않은 상태로 방치되는 것을 방지할 수 있는 암호화 모듈을 예로 들 수 있다.

컴파일 인증

컴파일 인증은 고급 프로그래밍 언어 의미론에서 얻은 정보를 이용하여 소스 코드를 컴파일하는 동안 인증서를 생성하는 발상이다.이 인증서는 소스코드가 특정 규칙 집합에 따라 컴파일되었다는 증명서를 소비자에게 제공하기 위해 컴파일된 코드와 함께 동봉되어야 한다.인증서는 예를 들어, 인증 코드(PCC) 또는 TAL(Typeed Assembly Language)을 통해 다양한 방법으로 제작될 수 있다.

증명-반송코드

PCC의 주요 측면은 다음과 같은 단계로 요약할 수 있다.[5]

  1. 공급자는 인증 컴파일러에 의해 생성된 다양한 주석을 가진 실행 가능한 프로그램을 제공한다.
  2. 소비자는 보안 정책에 기초하여 검증 조건을 제공한다.이것은 공급자에게 보내진다.
  3. 공급자는 프로그램이 실제로 보안 정책을 만족한다는 증거를 소비자에게 생산하기 위해 검증 조건을 정리하여 실행한다.
  4. 그러면 소비자는 증명서를 증명 검사기로 실행하여 증명 유효성을 검증한다.

인증 컴파일러의 예로는 PCC가 자바에서 구현한 프로그램에 대한 형식적인 유형 및 메모리 안전 증명을 제공하는 터치스톤 컴파일러가 있다.

입력된 어셈블리 언어

TAL은 유형 시스템을 사용하는 프로그래밍 언어에 적용된다.컴파일 후 오브젝트 코드는 일반 타입 체커로 확인할 수 있는 타입 주석을 휴대한다.여기서 생산되는 주석은 여러 가지 면에서 PCC가 제공하는 주석과 유사하며, 몇 가지 한계가 있다.그러나 TAL은 무엇보다도 메모리 안전과 제어 흐름을 포함할 수 있는 형식 시스템의 제한에 의해 표현될 수 있는 모든 보안 정책을 처리할 수 있다.

세미나

참조

  1. ^ "Can we learn from SCADA security incidents?" (PDF). www.oas.org. enisa.
  2. ^ "Air Traffic Control System Failed". www.computerworld.com. Retrieved 12 May 2014.
  3. ^ "Software Bug Contributed to Blackout". www.securityfocus.com. Retrieved 11 February 2004.
  4. ^ Pierce, Benjamin C. (2002). Types and Programming Languages. The MIT Press. ISBN 9780262162098.
  5. ^ Kozen, Dexter (1999). "Language Based Security" (PDF). Cornell University. {{cite journal}}:Cite 저널은 필요로 한다. journal=(도움말)

책들

  • G. Barthe, B. Grégoire, T. Rezk, 인증서 컴파일, 2008
  • 브라이언 체스와 게리 맥그로, 2004년 정적 보안 분석.

추가 읽기