고려대학교 행정학과

정형기법 연구실

최진영 교수

제가 고려대학교에 부임하던 1996년만 하더라도 정형기법은 국내에서는 아주 생소한 학문분야이고 이 단어조차 이해하는 분을 거의 만나기 어려웠습니다. 그러나, 최근에는 고 등급 소프트웨어의 중요성이 다양한 분야에서 커지면서 정형기법(Formal Methods) 라는 용어가 심심하지 않게 논문과 인구에 회자되고 있습니다.

정형기법은 소프트웨어 위기를 해결하기 위한 하나의 방법으로 1970년도에 정착된 분야입니다. 소프트웨어 위기는 간략히 말하면 “제대로 기능을 하는 프로그램을 만들 수 없다”라는 1960년도 시대적 혼란을 의미합니다. 그 이후 여러 원인이 제시가 되고 여러 처방이 나오게 되는 데, 정형기법은 다음과 같은 두가지 방법을 소프트웨어 공학에 제시하게 됩니다. 

1) 소프트웨어 요구사항을 명확하게 작성한다. 정형명세라고 하며, 모호하지 않은 명세를 작성하기 위해 수학적 기호를 주로 사용해서 요구사항을 작성하게 됩니다. 여기서 수학적 기호란 집합론, 명제논리, 술어논리, 고차논리 등을 포함한 수학적 논리학, 실시간 논리학, 행위를 표현하기 위한 프로세스 대수에서 정의되고 사용되는 기호를 의미합니다. 이렇게 하면, 매우 정확한 명세를 작성하게 되나, 사용하기가 매우 어렵습니다. (즉, 비용이 많이 들어갑니다.)

2) 소프트웨어 (설계/코드)가 원하는 속성을 만족한다는 것을 수학적 증명을 한다. 정형검증(Formal Verification)이라고 합니다. 설계 또는 구현물이 원하는 속성을 만족하는 지 수학적으로 증명을 하는 것입니다. 증명하는 것은 고전적 논리학 방법, 직관적 논리학 방법, 바이시뮬레이션 방법, 모델 체킹 방법등 다양한 방법이 활용되고 있습니다. 원하는 속성이 설계 또는 구현물이 만족하는 지 수학적으로 증명을 할 수 있으나, 역시 사용하기가 매우 어렵습니다.

이러한 정형기법은 처음에는 소프트웨어 공학의 한 분야로 발전을 하다가, 1996년 인텔 펜티움칩의 나눗셈 회로 버그 사건으로 하드웨어 기업에서 활용하게 되고, 이제는 하드웨어 설계시 필수적으로 사용하는 한 공학적 요소가 되었습니다. 이렇듯 소프트웨어, 하드웨어의 정형명세와 정형검증 기법은 시스템의 속성을 명세하고 검증하는 방법으로, 또는 프로토콜을 명세하고 검증하는 방법으로 활용이 되고 지금도 다양한 분야에서 사용이 되고 있습니다. 최근에는 4차 산업혁명의 핵심 요소로 인정받고 있는 System of System(SoS) 분야에서도 정형기법이 활용되고 있습니다.

이렇듯 정형기법은 소프트웨어/하드웨어/시스템의 기능에 대한 정확한 명세와 검증을 위해 사용이 되었습니다. 이러한 이유와 그리고 적용하기가 매우 까다롭고 비싼 이유로 소프트웨어 개발 시 전체 소프트웨어에 적용하는 것이 아니라, 기능성 분석 (예를 들면, 기능 안전성 분석)을 통해 정말 중요하고 핵심적인 부분만 정형기법을 적용하도록 하고 있습니다. 소프트웨어 안전 관련 첫 번째 국제 표준인 ISO 61508를 참조하시면 도움이 될 것으로 생각이 됩니다.

정형기법은 소프트웨어 등의 기능을 정확하게 정의된 명세대로 만들기 위하여 사용이 되다가, 소프트웨어 보안문제가 발생하게 되고, 이 역시 해결하는 하나의 방법으로 정형기법이 활용하게 됩니다. 소프트웨어가 명세된 대로 작동해야 한다는 속성인 SW Reliability (SW 신뢰성), 소프트웨어가 동작 중에 재난을 발생하면 안된다는 SW Safety (SW 안전성) 그리고 허가 받지 않은 외부 입력을 허용해서는 안된다는 SW Security (SW 보안성) - 여기서 말하는 소프트웨어 속성은 소프트웨어 공학에서 일반적으로 사용하는 정의입니다. 다른 분야에서는 다르게 정의되고 사용될 수 있습니다.) 즉, 소프트웨어 보안성이라는 새로운 속성을 정의하고 검증하는 데, 정형기법이 활용이 되고 있습니다.

소프트웨어 보안 속성을 만족하는 프로그램을 만들기 위해 (제로데이) 취약점의 원인이 되는 보안약점이 없는 소프트웨어를 만들어야 합니다. 정형기법은 이러한 소프트웨어를 만드는 데 활용이 되고 있으며, Common Criterial에서 EAL 5 등급이상에서 부분별로 정형기법을 사용하도록 요구하고 있습니다.

소프트웨어 중심 사회, 스마트 사회로 진입을 하며, 소프트웨어의 중요성이 더욱 더 요구되고 있으며, 특히 안전이나 보안에 강인한 소프트웨어를 만드는 고급기술이 더욱 필요해 지고 있습니다. 소프트웨어는 전통적으로 소프트웨어 품질 보증 (SW Quality Assurance) 와 소프트웨어 보안 보증 (Software Sequrity Assurance) 로 구분이 되었었는 데, 이제는 이러한 두 종류의 보증이 소프트웨어 보증 (Software Assurance) 한 개념으로 통합이 되고 있습니다. 여기에서도 역시 고 등급의 경우 정형기법이 핵심요소로 자리매김을 하고 있습니다.

본 정형기법 연구실에서는 이러한 정형기법에 관한 연구를 1996년부터 국내 처음 시작하였습니다. 당시 고려대학교 컴퓨터학과 소속이였으며, 행안부 지원 소프트웨어개발보안연구센터 와 고품질소프트웨어공학센터(ITRC)를 함께 운영을 하였습니다. 지금은 정보보호대학원 소속으로 미래 소프트웨어를 정형기법을 이용한 보안 과 안전성 중심으로 연구를 하고 있습니다.  

"Those who will be able to conquer software will be able to conquer the world.“ - Tadahiro Sekimoto, former president, NEC Corp