[Translation] Righting Software

[Translation] Righting Software

--- James R.   Larus, Thomas Ball, Manuvir Das,  Robert DeLine, Manuel

    Fahndrich,  Jon   Pincus,  Sriram  K.   Rajamani,  and  Ramanathan

    Venkatapathy

[번역] 소프트웨어의 안전성 향상

주제: 마이크로소프트에서 개발한 소프트웨어 안전성 향상을 위한 도구

1세대 도구

특징: AST 탐색, symbolic execution, unsound

      PREfix

      -- 프로그램  call  그래프의  bottom-up으로  탐색하며  각  함수의

         모델을 만들어 그 함수를 호출했을 때 효과를 기록

      -- null  pointer  reference,   improper  memory  allocation  and

         deallocation,  use of  uninitialized values,  simple resource

         state errors, and improper library use 등을 검사

      PREfast

      -- local 분석

      -- 프로그래밍 idiom을 검사

2세대 도구

특징: 첫째, declarative descriptions for program behavior를 정의 확장 가능., 

      둘째, sound program analysis를 사용

      Slam

      -- API 순서에 대해 검사 (예, acquirelock(), releaselock())

      -- 검사하고자 하는 바에 대한 룰을 FSM으로 정의

      -- 분석 대상 프로그램을 룰에 대해서 boolean 프로그램으로 변환.

         (원래 프로그램의 control flow construct, boolean variable만 포함)

      -- boolean 프로그램에 대해서 룰을 적용하고 룰에 따르지 않는 path를

         찾음

      -- 원래  프로그램의  해당  path를  symbolic  execution하고  만일

         feasible하면 에러를 찾은 것임. feasible하지 않으면 (그 path가

         사실을    가능하지   않은    것인데    boolean   프로그램으로

         단순화하다보니  가능한 것  처럼 보인  path라면) 그  path가 왜

         feasible하지  않은지에   대한  이유를  설명해주는  predicates

         (control flow에서  조건식?)을 구한다. 이  predicates을 가지고

         처음   boolean  프로그램을   더  세분화해서   새로운  boolean

         프로그램을  만든  다음   이  프로그램의  모든  path에서  룰을

         적용해서 모든 path가 룰을 지킨다는 것을 검증한다.

      -- Slam이  Windows   Device  Driver에  적용해서   성공한  이유는

         드라이버  프로그램의 안전성  규칙은 커널  리소스  사용에 달려

         있고, Slam은 데이터를  하드웨어에 보내고 받는 드라이버 부분을

         단순화하고 제어 흐름을 검사하는데 집중할 수 있기 때문이다.

      ESP

      -- Path-sensitive Program verification in polynomial time

      -- Error  detection   via  scalable  program   analysis  (Slam과

         비교해서 모델 체킹 대신 프로그램 분석을 사용한 점이 다름)

      -- OPAL 규칙으로 C, C++ 코드 검증

      -- OPAL  (Object Property  Automata  Language): FSM과  syntactic

         code 패턴

         OPAL 언어로 기술하는 규칙의 예

         - 상태: Closed, Opened, Erros.

         - 이벤트 발생 조건: "fopen" 심볼에 Open 이벤트 발생, "fclose"

           심볼에 Close 이벤트 발생

         - 이벤트에 따른 상태 전이 규칙

      -- ESP 분석 엔진

         첫번째  가능한  전략,  프로그램의  각  path를  따라  symbolic

         execution  하면서  각 event에  따라  OPAL  규칙에 따라  FSM을

         변경한다. 하나의 규칙에 관련된 branch는 상당히 떨어져 있을 수

         있고 (예를 들어 fopen과 fclose) 이것들의 상관 관계를 연관짓는

         정도의 symbolic execution은 매우 비싼 계산이 필요하다.

  두번째 전략,  path를 따라 분석하지 않고  각 프로그램 포인트에

  FSM의 상태를  연관지으면 분석을 빨리  할 수 있지만  매우 많은

  false error를 낼 것이다.

  채택한 전략, 특정  규칙은 대부분의 branch와 무관하다는 관찰에

  의존한다.   ESP 분석  엔진은 `관련이  있는'  branch를 찾는다.

  조건문이 관련이  있다는 것은 규칙의  object의 상태가 조건문의

  branch에  따라  다른 상태로  변하는  경우이다. 관련이  없다면

  branch  correleation을 무시한다.  polynomial  time 분석  계산

  시간의 이유이다.

  복잡한 alias 분석, value 흐름 분석을 사용

      Vault

      -- A safe  version of C, 

      -- 인터페이스의   타입  signature에서   API를   어떻게  사용해야

         하는지를 타입으로 기술하고  사용자가 이를 제대로 사용하는지를

         타입 검사를 통해 확인

      -- 프로그래머가 직접 타입을 기술해야 함, 모듈 단위 체킹이 가능

     

      -- interface에서  abstract  states를  프로그램  객체와  연결하고

         연산을  수행할  때  필요한  precondition과  post  condition을

         지정하는 규칙을 지정.

      -- capability-based 객체  tracking, linear 타입으로 non-aliasing

         보장