페이퍼요약 - 높은 무결성의 의료 기기 소프트웨어 개발을 위한 견고한 검증 기법 by Abraham

제목: 높은 무결성의 의료 기기 소프트웨어 개발을 위한 견고한 검증 기법(Sound Verification Techniques for Developing High-Integrity Medical Device Software)

저자: Jay Abraham 외 2인, The MathWorks, 미국

문서유형: 컨퍼런스 페이퍼(총 10페이지), 2009년

 

의료 기기 소프트웨어의 에러 검증에 대한 전반적인 설명을 하고, 정형적 검증 방법(formal methods) 중 하나인 추상적 해석(Abstract Interpretation) 기법을 이용한 런타임 에러 검증에 대해 설명한 자료. 또한 이 추상적 해석 기법을 지원하는 도구인 MathWorks사의 PolySpace도 소개 

---

배경 정보

• 의료 기기의 임베디드 소프트웨어 규모 및 복잡도 증가: 최첨단 페이스케이커(pacemakers)는 8만 라인의 코드를 포함하고 있고, 주사액주입기(infusion pumps)는 17만 라인 이상의 코드로 구성
• 소프트웨어 코딩 에러로 인한 의료 기기의 결함 증가: Bliznakov의 연구에 따르면 1999년~2005년 동안 FDA 리콜의 11.3%가 소프트웨어 코딩 에러에 기인
• 방사선치료기기(a radiation therapy device)의 소프트웨어 코딩 에러로 인해 다수의 환자가 과다 투여로 죽음에 이르는 사고가 발생한 1980년대 중반부터 의료 기기 소프트웨어 개발에 대한 FDA의 감독이 강화됨. FDA는 좋은 소프트웨어 개발 프로세스에 대한 여러 표준과 가이드 문서를 발간하고, 리콜 조사 대상 의료 기기의 소프트웨어 코딩 에러를 식별하기 위한 소프트웨어 연구실도 설립함. 이 연구소는 리콜 조사의 일환으로 소스 코드를 분석하여 기기 장애(failure)의 근본 원인(the root cause)을 이해하고 식별한다.
• 의료 기기 소프트웨어 검증을 위해 일반적으로 수행되는 방법들로 코드 리뷰(code reviews), 정적 분석(static analysis), 동적 테스트(dynamic testing)가 있다. 코드 리뷰는 검토자의 개인 역량(전문성)에 크게 의존하며 큰 규모의 코드에서는 비효율적일 수 있다. 전통적인 정적 분석 기법들은 불안전한 코드 패턴(unsafe code patterns)을 찾아내는 패턴 매칭법(a pattern-matching approach)에 주로 의존하지만 런타임 에러가 없다는 것을 증명하지는 못한다. 동적 테스트에서는 기기 소프트웨어 규모가 커짐에 따라 모든 운영 조건을 동적으로 테스트 하는 것이 거의 불가능하다.

임베디드 기기 장애 사례(Embedded Device Failures)

• 방사선 치료 기기 Therac 25: 이 기기의 실시간 운영체제(RTOS)가 쓰레드 메시지 패싱을 지원하지 않아서 대신 전역 변수(global variables)가 사용됨. 전역 변수의 무결성 보호가 미흡하여 결과적으로 기기 동작 중에 잘못된 데이터를 사용. 또한 8비트 정수 카운터(an 8 bit integer counter)의 오버플로우 문제도 발생. 이런 소프트웨어 코딩 에러들로 인해 처방된 투여량의 30배가 되는 방사선이 환자에게 투여됨
• 로켓 Ariane 5: 첫 발사 시 발사대가 파괴되어 피해 발생. 로켓의 자세를 결정하는 한 쌍의 관성기준시스템(Inertial Reference Systems)에서 오버플로우가 발생한 것이 원인. 이 오버플로우는 64비트 부동 소수점 수(a 64 bit floating point number)를 16비트 정수(a 16 bit integer)로 전환하는 과정에서 발생. 중복 시스템을 두어 설계하였지만 백업 시스템도 똑같은 동작으로 구현되었기 때문에 도움이 안됨
• 우주 왕복선 시뮬레이터(Space Shuttle Simulator): 실행의 중지(abort) 과정에서 왕복선의 4개의 메인 컴퓨터가 모두 다운됨. 코드 조사 결과 연료 관리 소프트웨어(the fuel management software)에서 문제 발생. 일차적인 연료 덤프가 실행된 후 카운터들을 올바르게 재초기화(reinitialized)하지 않아서 결과적으로 코드가 메모리의 랜덤 영역(random sections of memory)으로 점프하고 컴퓨터를 다운시킴

런 타임 에러

런 타임 에러를 일으키는 잘못 작성된 코드가 위 예시된 임베디드 기기 장애의 주요 원인이다. 런 타임 에러는 잠복성(Latent faults)을 가지는 소프트웨어 에러의 한 유형으로서, 코드에 존재하더라도 특정 조건하에서 특정 테스트를 수행하지 않는 한 찾기가 어렵다. 따라서 기능적으로 정상으로 동작하는 것처럼 보여도 예상치 못한 시스템 장애를 가져올 수 있다. 런 타임 에러의 원인으로 아래와 같은 몇 가지를 들 수 있다.

• 초기화가 안된 데이터(Non-initialized data): 변수가 초기화가 안된 경우 임의의 값으로 변수값이 설정될 수 있는데, 이런 변수를 사용하는 프로그램은 의도한 대로 작동하다가도 특정 조건에서 예상치 못한 결과를 낼 수 있다.
• 경계 범위 밖 접근(Out of bounds array access): 할당된 메모리의 경계를 넘어 데이터 쓰기나 읽기가 이루어질 때 발생하는 에러로 프로그램 실행 중 예상치 못한 결과를 낼 수 있다.
• 널 포인터 참조 해제(Null pointer dereference): NULL 상태인 포인터로 메모리를 참조하려 할 때 발생. 메모리에게 있어 이건 유효값이 아니므로(a “non-value” for memory) 해당 포인터의 참조 해제 시도는 바로 시스템 다운으로 이어진다.
• 부정확한 계산(Incorrect computation): 산술 연산에서 오버플로우, 언더플로우, 0으로 나누기(divide by zero), 음수값의 제곱근(a square root of a negative number) 사용 등으로 인해 발생되는 에러로서 프로그램을 다운시키거나 잘못된 결과값을 산출한다.
• 공용 데이터에 동시 접근(Concurrent access to shared data): 서로 다른 쓰레드에 있는 두 개 또는 그 이상의 변수들이 메모리의 같은 위치를 접근하려 할 때 발생하는 에러. 리소스 경쟁 상황(race condition)이 발생하거나, 보호되지 않은 형태로 여러 쓰레드가 공용 데이터에 접근하는 것을 허용함에 따라 데이터가 손상되는 결과를 초래한다.
• 허용되지 않는 타입 전환(Illegal type conversions): 부적절하게 타입을 전환하여 데이터를 손상시키거나 의도하지 않은 결과를 산출한다.
• 절대 실행되지 않는 죽은 코드(Dead code): 데드 코드가 직접적으로 런타임 에러를 유발하지는 않을지라도 왜 프로그래머가 그런 코드를 작성하였는지 이해하는 것이 중요할 수 있다. 데드 코드는 코딩 능력이 떨어진다거나 설계 명세서(프로그램 명세서)가 존재하지 않는다든지 등의 문제점을 알리는 신호이다.
• 무한 루프(Non-terminating loops): 프로그램 루프 구문(예, for, while 등)에서 부정확한 조건문(incorrect guard conditions) 사용으로 발생하는 문제로서 시스템 멈춤(system hangs or halts)을 유발할 수 있다.

정형적 검증 방법(Formal methods)

• 시스템 명세(specifications)를 기준으로 하는 증명 기반의 검증(proof based verification) 방법
• 코드의 정확성을 수학적으로 엄격하게 증명하는 방법
• 이 페이퍼에서 런타임 에러 부재를 증명하는 기법으로 활용된 추상적 해석(Abstraction Interpretation)도 Formal method의 일종

추상적 해석(Abstract Interpretation) 기법

1) 기본 개념

아래 산술식의 결과값을 손으로 바로 계산하는 것은 어렵지만 계산 결과를 기호 영역(the sign domain)으로 추상화하면 결과값이 음수라는 것을 쉽게 알 수 있다.

예) -4586 × 34985 × 2389 = ?

 

추상적 해석(Abstract Interpretation) 기법은 최종 결과값의 일부 속성(properties)을 정확하게 파악하는 것을 가능하게 해준다. 위 예에서는 계산식을 완전히 계산하지 않고도 결과값의 기호가 음수라는 것을(그리고 절대 양수가 될 수 없다는 것을) 알아낼 수 있었다. 따라서 프로그램 정확성 검증 시 추상적 해석 기법은 “위 오퍼레이션의 기호가 항상 음수이고 절대 양수가 되어서는 안되다”는 것을 증명한다.

추상적 해석(Abstract Interpretation)의 수학적 표현에서 프로그램 언어로 작성된 실제 프로그램을 S라 하고 이 프로그램의 추상화 버전을 A라 했을 때 실제 영역에서 추상화 영역으로 매핑하는 추상화 함수를 a, 추상화 영역 A에서 실제 영역 S로 매핑하는 함수는 g라 한다. a와 g는 갈루아 대응(a Galois connection)을 형성하며 단조 함수(monotonic)이다.  

추상적 해석 기법은 추상화 영역 A에서 소프트웨어의 특정 속성(properties)에 대한 증명을 한다. 실제 영역 S에 비교해서 추상화 영역 A에서의 증명(proof of correctness)은 훨씬 간단히 수행 가능하다.

 

추상적 해석 기법 적용을 위해서는 검증 대상의 소프트웨어 코드를 추상화 함수 a를 기반으로 하여 유사한 추상화 버전으로 계산하는 작업이 필요한데, 이 때 실제 프로그램의 추상화된 의미(the program’s abstract semantics)를 표현한 여러 등식(equations) 및 제약 조건(constraints)이 생성된다.

 

추상적 해석 기법은 변수 값을 표현하기 위해 격자(Lattices)를 사용한다. 위의 기호(sign) 관련 예에서는 아래 그림과 같은 격자가 프로그램의 변수 값들의 추상화를 위해 사용될 수 있다.

2) 런 타임 에러 증명에 적용 예

소프트웨어 프로그램의 특정 속성을 증명하는 추상적 해석 기법을 런타임 에러가 소프트웨어에 존재하지 않는다는 것을 증명하는 용도로 적용 가능하다. 예를 들면 간단한 코드 X = X/(X-Y) 에서 런 타임 에러가 발생할 수 있는 원인으로 아래와 같은 것을 들 수 있다.

• 변수가 초기화 되지 않음
• 빼기 오퍼레이션 (X-Y)에서 오버플로우 또는 언더플로우 발생
• 나누기 오퍼레이션에서 오버플로우 또는 언더플로우 발생
• X가 Y와 동일하면 0으로 나누기(a divide by zero) 문제 발생
• X에 값이 할당될 때 오버플로우 또는 언더플로우 발생

 

이 중 4번째의 divide by zero 분석 해 보면, X와 Y의 가능한 값들이 흩뿌려진(+로 표시됨) 아래 그래프에서 빨간색의 45도 선이 X=Y인 경우(즉, divide by zero 런 타임 에러가 발생하는 경우)를 나타낸다.

동적 테스트는 divide by zero 런 타임 에러의 부재를 증명하기 위해 X와 Y의 무수한 조합을 일일이 실행해야 하므로 비효율적이다. 또 다른 방법은 타입 분석(type analysis)을 통해 런 타임 에러 조건(즉, X=Y)에서의 X와 Y의 범위를 알아내는 것이다. 아래 그림에서 경계를 나타내는 박스가 타입 분석을 통해 얻어진 정보이다. 이 박스가 X=Y를 교차할 때 런타임 에러가 발생할 가능성이 있다. 하지만 이 타입 분석 방법도 비현실적인 X와 Y의 값들을 모두 포함하므로 역시 효율성이 그다지 높지 않다.

추상적 해석 방법을 사용하면 X와 Y의 좀 더 정확한 데이터 범위 표현이 가능하다. X와 Y 값에 다양한 프로그래밍 구문(예, pointer arithmetic, loops, if-then-else, multitasking 등)이 X와 Y의 값에 영향을 줄 수 있으므로, 추상화 격자(an abstract lattice)를 정의하여 아래 그래프처럼 데이터 그룹을 다면체로 표현한다. 다면체들이 X=Y와 교차하지 않으므로 division by zero 에러가 발생하지 않는다고 결론 내린다.

추상적 해석 기법 지원 도구인 PolySpace

MathWorks사의 PolySpace는 Abstract Interpretation 기법을 활용하는 코드 검증 제품이다. C, C++, 또는 Ada 소스 코드를 입력으로 받아서 아래의 4가지 색으로 품질 분석 결과를 표시한 소스 코드를 출력한다.

• 녹색: 신뢰할 수 있는 코드
• 빨강: 잘못된 코드로 인한 런 타임 에러
• 회색: 접근이 불가능한 죽은 코드(dead or unreachable code)
• 오렌지색: 검증 안된 코드(Unproven code)

 

예를 들면 아래의 where_are_errors() 소스 코드는 라인 17에서 x=y인 경우에 divide by zero가 발생할 가능성이 있다. 

PolySpace가 이 소스 코드를 입력 받으면 아래와 같은 분석 결과를 보여준다. 

PolySpace의 결과에 따르면 이 코드에는 런 타임 에러가 없다(모두 녹색으로 표시). 라인 17은 (3*k + 100 > 43) 조건이 참인 경우에만 실행되고 또한 y의 값이 k의 값에 의존하기 때문에 라인 17에서 x는 10일 때 y는 항상 10보다 큰 값을 가진다(즉, divide by zero 에러가 발생하지 않는다).

 

PolySpace는 코드를 실행하거나, 테스트 케이스를 작성하거나, 소스 코드에 계측 코드(instrumentation)를 삽입하거나, 또는 디버깅을 한다든지 할 필요 없이 런 타임 에러 유무를 분석해 내므로 효율적이다. 위 결과에서 밑줄이 쳐진 코드는 잠재적으로 런 타임 에러를 가질 수 있는 부분을 나타낸다.