Symbolic Testing

COYOTE는 소프트웨어의 각 함수에 대하여 테스트케이스를 자동생성하고 테스트케이스에 대한 실행 테스트를 자동으로 실행합니다.

완전 자동 테스팅을 실현할 때 가장 어려운 부분이 바로 테스트케이스 자동생성입니다. 수십 년 동안 다양한 기법들이 고안되었지만 고전을 면치 못했습니다. 많은 테스트 자동화 도구들이 테스트케이스 자동생성 기능이 있다고 광고하고 있지만, 현장에서는 외면 받아온 이유입니다.
우리는 테스트케이스 자동생성을 실용화 수준으로 가능하게 하는 심볼릭 테스팅 엔진을 순수 국산기술로 개발하였습니다. 심볼릭 테스팅 기술은 심볼릭 실행(symbolic execution) 또는 콘콜릭 실행(concolic execution) 기법을 이용하여 화이트박스 테스팅을 수행하며, 테스트케이스 자동생성에 탁월한 능력을 발휘합니다.

심볼릭 테스팅 엔진은 주어진 함수의 모든 실행 경로를 탐색하면서 각 실행 경로가 실행되는 조건(경로 조건)을 계산합니다. 그리고 이 경로 조건을 이용하여 각 경로에 대한 테스트케이스를 생성합니다.

이를 위해서는 심볼릭 연산을 수행할 코드를 주어진 함수에 삽입하고 그 함수를 구동할 드라이버 코드와 그 함수가 호출하는 다른 함수의 스텁 코드를 생성함으로써 테스트 실행파일을 자동생성합니다. 테스트를 구동하면 실제 실행과 심볼릭 실행을 동시에 진행하면서 경로 조건과 테스트케이스를 계산합니다. 이때 조건식 해결을 위해서는 SMT 해결기와 같은 자동 정리증명기를 사용합니다.

자동검증팀

“우리는 콘콜릭 실행, 자동정리증명, 정적 분석, 머신 러닝 등의 기술을 융합하여 완전 자동 테스팅 도구를 개발합니다.”
“개발환경은 F# 같은 함수 언어와 Java 같은 객체지향 언어 등을 주로 사용합니다.”
“심볼릭 테스팅 기술 뿐아니라 자동 테스팅에 필요한 다양한 요소들을 자동화하는데에는 소스코드 분석, SMT 해결기, 코드 생성 기술 등이 중요한 역할을 합니다.”
“자동차, 항공 등 SW 신뢰성이 특히 중요한 분야에서 완전 자동 테스팅 도구 COYOTE가 든든한 동반자가 되도록 최선을 다하겠습니다.”

Static Analysis

소스코드 진단 도구인 CODEMIND CSI/CQI는 소스코드에 내재된 보안 약점을 찾아내고 실행 중 발생 가능한 오류를 미리 검출합니다.

소프트웨어의 동작을 실행하지 않고 미리 예측하는 기술을 통틀어 정적 분석이라고 합니다. 정적 분석은 타입 분석, 데이터 흐름 분석, 제어 흐름 분석, 정보 흐름 분석, 메모리 모양 분석 등 다양한 기법으로 나타날 수 있습니다.

댜양한 정적 분석 기법을 하나의 프레임워크 안에서 설계할 수 있도록 고안된 것이 요약 해석(abstract interpretation) 기술입니다. 요약 해석을 기반으로 다양한 시맨틱 분석을 체계적으로 구현할 수 있어서 정적 분석의 표준으로 자리잡고 있습니다.

요약 해석의 원리는 주어진 프로그램을 추상화된 연산을 통해 추상화된 값을 계산하는 것입니다. 예를 들어, 아래의 간단한 프로그램에 대해서 각 지점의 x 값이 가질 수 있는 범위를 계산하는 연립방정식을 만들어냅니다. 이 연립방정식의 해를 고정점이라 하고 반복적인 방법으로 고정점을 계산해냅니다.

이런 방식으로 변수의 값을 계산하거나 메모리 할당 모양을 예측해냅니다. 두번째 그림은 주어진 프로그램의 메모리 모양을 요약 해석을 통해서 계산하는 과정입니다. 여기서는 메모리 분석 결과로부터 반환된 포인터 접근(Use after Free) 오류를 검출하는 예를 보여줍니다.

또한 CODEMIND는 정적 분석 엔진을 그래프 DB를 활용하여 구현하였는데, 분석 결과를 온더 플라이 방식으로 분석 중에 확인할 수 있으며, 편리한 결함 추적 그래프를 생성하는 데에도 유용합니다.

정적분석팀

“우리는 요약해석 기반 정적분석 도구를 개발합니다. 구문분석, 흐름분석, 메모리분석, 값분석 등을 이용하여 시큐어코딩 진단과 품질 진단을 제공합니다.”
“개발환경은 Scala 같은 함수 언어와 Java 같은 객체지향 언어 등을 복합적으로 사용합니다.”
“우리는 국내 최초로 그래프 DB 기반 분석과 시맨틱 기반 분석을 융합하여 온더 플라이 진단을 구현하고 결함추적 그래프를 제공할 수 있었습니다.”
“최근에는 고객마다 개발 환경과 진단 요구 사항이 다양하게 제시되고 있어서 고객 맞춤형 도구 제공이 중요해지고 있습니다. 앞으로도 SW 보안과 안전에 대한 고객 요구를 만족시키기 위해 최선을 다하겠습니다..”