다양한 환경에서 소프트웨어의 오류를 파악하는 소프트웨어 테스팅...정형검증 필수
[보안뉴스= 고기혁 KAIST 사이버보안연구센터 AI보안팀장] 인공지능 기술은 인공지능 비서, 자율주행 자동차 등 고도로 복잡한 작업까지 문제없이 수행할 만큼 눈부신 발전을 이루어 왔습니다. 특히, 일일이 그 작동 원리를 명시하지 않아도 데이터를 통해 알아서 학습해 스스로 작동 원리를 깨우치는 학습 기반 인공지능은 훌륭한 성능과 함께 그 개발에 드는 비용의 감축으로 인공지능의 진정한 상용화를 이끌어 왔습니다.
하지만 인공지능의 활용에는 그에 따른 부작용의 위험 또한 존재합니다. 이는 데이터를 기반으로 학습되는 인공지능이 어떤 원리로 작동하는지 이해하기 어렵기 때문입니다. 실례로 자율주행 자동차, 주식투자 인공지능 등에서 발생한 오류로 인해 인명 및 재산 피해가 발생한 바 있으며, 이와 같은 인명 및 재산 피해를 막기 위해서는 인공지능의 안전성 검증이 필수적입니다.
복잡한 인공지능이 안전하게 작동하는지를 판단하는 가장 간단한 방법은 여러 가지 상황에서 테스트해보는 것입니다. 자율주행 자동차를 예로 들자면, 다양한 도로나 횡단보도, 교차로의 모양이나 신호등의 타이밍, 날씨 및 주행 시간 등 수많은 상황에서 사고 없이 잘 동작하는지를 확인하는 것이죠. 이처럼 다양한 환경에서 작동하여 봄으로써 주어진 소프트웨어의 오류를 파악하는 것을 ‘소프트웨어 테스팅(Software Testing)’이라고 합니다.
소프트웨어 테스팅은 다양한 시나리오 하에서 소프트웨어를 작동시켜 보기만 하면 되어 비교적 간단하다는 장점이 있는 반면, 테스팅을 통해 시험해보지 못한 시나리오에서 오류가 발생할 가능성이 있다는 단점이 있습니다. 가능한 모든 상황을 고려하지 않는다면 ‘오류가 절대로 발생할 수 없다’와 같은 보장을 얻기는 불가능한데, 모든 상황을 고려한다는 것은 현실적으로 불가능하기 때문입니다. 이와 같은 문제점을 해결하고 오류가 존재하지 않는다는 ‘절대적인 보장’을 얻기 위하여 소프트웨어를 논리적으로 분석함으로써 오류가 존재할 수 없음을 엄밀하게 증명하는 방법을 ‘정형 검증(Formal Verification)’이라 합니다.
정형 검증은 크게 세 단계를 통해 진행됩니다. 먼저 주어진 소프트웨어에 대해 그 작동 기작을 나타내는 수학적 모델을 설립하고, 다음으로는 검증하고자 하는 속성을 논리적 언어로서 명세합니다. 마지막으로 소프트웨어의 수학적 모델이 검증하고자 하는 속성을 지닌다는 것을 증명하거나 속성을 위반하는 예시인 반례를 찾음으로서 속성을 지니지 않는다는 것을 보일 수 있습니다.
예를 들어, 횡단보도가 있는 직선 도로에서 자동차 신호등과 보행 신호등의 신호를 제어하는 소프트웨어를 생각해 봅시다. 이 소프트웨어는 시간에 따라 자동차 신호등과 보행 신호등의 색깔, 즉 자동차 신호등의 색깔이나 보행 신호등의 색깔의 상태를 변화시키는 간단한 그래프 모델로 생각할 수 있습니다. 차도에 자동차가 주행 중일 때는 녹색(보행은 빨강)이던 신호가 노란불이 켜지면서 노랑(보행은 빨강)이 되었다가, 보행자가 횡단보도를 건널 수 있는 빨강(보행은 녹색) 신호로 변화하는 것이죠. 보행자 신호가 끝나면 다시 원상태인 녹색(보행은 빨강)으로 돌아가 자동차가 주행 가능한 신호로 변화할 것입니다.
앞서의 도로 상황에서 보행자와 자동차 모두 안전하기 위해서 보행 신호등은 자동차 신호등이 빨간색일 때만 녹색불로 켜져야 할 것입니다. 즉, 빨강-녹색은 가능해도 녹색-녹색이나 노랑-녹색과 같은 상태는 있을 수 없다는 것입니다. 이는 위에서 그래프로 표현한 소프트웨어의 구동 단계에서는 발생할 수 없음을 볼 수 있으며, 따라서 소프트웨어가 녹색-빨강의 초기 상태로 구동되는 한 안전함을 보일 수 있습니다.
이와 같은 정형 검증 기법은 인공지능 모델에 대해 적용하기는 여러 가지 어려움이 있습니다. 이는 인공지능 모델과 전통적인 소프트웨어의 구조 및 기능적 차이 때문으로, 먼저 인공지능 소프트웨어에 주어지는 입력이 전통적인 소프트웨어에 주어지는 입력에 반해 매우 복잡합니다. 앞서의 신호등 예시에서 소프트웨어에 주어지는 입력은 초기 상태뿐인 반면, 실제 인공지능 소프트웨어에서는 음성, 이미지, 텍스트 등 고차원의 입력이 주어집니다. 고차원의 입력에 따라 소프트웨어에 무수히 많은 상태들이 생겨날 수 있는 것이죠.
또 다른 어려움은 인공지능 소프트웨어가 작동하는 정확한 원리를 알기 어렵다는 점에서 기인합니다. 정형 검증 방법론을 적용하기 위해서는 주어진 소프트웨어를 수학적인 모델로서 표현해야 하는데, 여기에는 그 작동 원리를 파악하고 이에 따라 ‘압축’해 수학적인 모델을 설립하는 과정이 포함됩니다. 전통적인 소프트웨어는 한 줄 한 줄 실행되는 프로그램 형태를 띠고 있어 그 압축이 용이한 반면, 인공지능 모델은 복잡한 함수의 집합체로 표현되어 압축하는 것이 매우 어렵습니다.
안전성을 올바르게 수학적으로 명시하는 것 또한 매우 어렵습니다. 자율주행 자동차가 ‘빨간불일 때 속도를 줄인다’거나 ‘사람이 앞에 있을 경우 멈춘다’는 안전성을 지키게 하기 위해서는 먼저 ‘빨간불이 켜져 있음’ 혹은 ‘사람이 앞에 있음’ 등의 조건을 수학적으로 정의해야만 하는데, 이는 불가능에 가깝다고 할 수 있습니다. 덧붙여, 여러 가지 서로 다른 조건에서 파생된 안전성을 동시에 만족하게끔 명시하는 것은 더더욱 어려울 것입니다.
만약 이 모든 어려움을 해결하고 인공지능 소프트웨어의 안전성을 완벽하게 검증했다고 하더라도 실질적인 상황에서 활용 시 문제가 생길 수 있습니다. ‘직진 주행 중에는 차선을 벗어나지 않는다’는 안전성이 검증된 자율주행 자동차가, 응급 환자를 싣고 급히 달려가는 응급차를 위해 잠시 가던 길을 멈추고 살짝 틀어 길을 양보해주는 것이 가능하지 않을 것임은 뻔히 보이는 일입니다. 인공지능의 안전성 검증은 안전성 그 자체뿐만 아니라 실제 인공지능이 활용되는 상황을 면밀히 고려해야만 올바르게 해결할 수 있는 문제인 것입니다.
[글_ 고기혁 KAIST 사이버보안연구센터 AI보안팀장]
[보안뉴스= 고기혁 KAIST 사이버보안연구센터 AI보안팀장] 인공지능 기술은 인공지능 비서, 자율주행 자동차 등 고도로 복잡한 작업까지 문제없이 수행할 만큼 눈부신 발전을 이루어 왔습니다. 특히, 일일이 그 작동 원리를 명시하지 않아도 데이터를 통해 알아서 학습해 스스로 작동 원리를 깨우치는 학습 기반 인공지능은 훌륭한 성능과 함께 그 개발에 드는 비용의 감축으로 인공지능의 진정한 상용화를 이끌어 왔습니다.
[이미지=utoimage]
하지만 인공지능의 활용에는 그에 따른 부작용의 위험 또한 존재합니다. 이는 데이터를 기반으로 학습되는 인공지능이 어떤 원리로 작동하는지 이해하기 어렵기 때문입니다. 실례로 자율주행 자동차, 주식투자 인공지능 등에서 발생한 오류로 인해 인명 및 재산 피해가 발생한 바 있으며, 이와 같은 인명 및 재산 피해를 막기 위해서는 인공지능의 안전성 검증이 필수적입니다.
복잡한 인공지능이 안전하게 작동하는지를 판단하는 가장 간단한 방법은 여러 가지 상황에서 테스트해보는 것입니다. 자율주행 자동차를 예로 들자면, 다양한 도로나 횡단보도, 교차로의 모양이나 신호등의 타이밍, 날씨 및 주행 시간 등 수많은 상황에서 사고 없이 잘 동작하는지를 확인하는 것이죠. 이처럼 다양한 환경에서 작동하여 봄으로써 주어진 소프트웨어의 오류를 파악하는 것을 ‘소프트웨어 테스팅(Software Testing)’이라고 합니다.
소프트웨어 테스팅은 다양한 시나리오 하에서 소프트웨어를 작동시켜 보기만 하면 되어 비교적 간단하다는 장점이 있는 반면, 테스팅을 통해 시험해보지 못한 시나리오에서 오류가 발생할 가능성이 있다는 단점이 있습니다. 가능한 모든 상황을 고려하지 않는다면 ‘오류가 절대로 발생할 수 없다’와 같은 보장을 얻기는 불가능한데, 모든 상황을 고려한다는 것은 현실적으로 불가능하기 때문입니다. 이와 같은 문제점을 해결하고 오류가 존재하지 않는다는 ‘절대적인 보장’을 얻기 위하여 소프트웨어를 논리적으로 분석함으로써 오류가 존재할 수 없음을 엄밀하게 증명하는 방법을 ‘정형 검증(Formal Verification)’이라 합니다.
정형 검증은 크게 세 단계를 통해 진행됩니다. 먼저 주어진 소프트웨어에 대해 그 작동 기작을 나타내는 수학적 모델을 설립하고, 다음으로는 검증하고자 하는 속성을 논리적 언어로서 명세합니다. 마지막으로 소프트웨어의 수학적 모델이 검증하고자 하는 속성을 지닌다는 것을 증명하거나 속성을 위반하는 예시인 반례를 찾음으로서 속성을 지니지 않는다는 것을 보일 수 있습니다.
예를 들어, 횡단보도가 있는 직선 도로에서 자동차 신호등과 보행 신호등의 신호를 제어하는 소프트웨어를 생각해 봅시다. 이 소프트웨어는 시간에 따라 자동차 신호등과 보행 신호등의 색깔, 즉 자동차 신호등의 색깔이나 보행 신호등의 색깔의 상태를 변화시키는 간단한 그래프 모델로 생각할 수 있습니다. 차도에 자동차가 주행 중일 때는 녹색(보행은 빨강)이던 신호가 노란불이 켜지면서 노랑(보행은 빨강)이 되었다가, 보행자가 횡단보도를 건널 수 있는 빨강(보행은 녹색) 신호로 변화하는 것이죠. 보행자 신호가 끝나면 다시 원상태인 녹색(보행은 빨강)으로 돌아가 자동차가 주행 가능한 신호로 변화할 것입니다.
앞서의 도로 상황에서 보행자와 자동차 모두 안전하기 위해서 보행 신호등은 자동차 신호등이 빨간색일 때만 녹색불로 켜져야 할 것입니다. 즉, 빨강-녹색은 가능해도 녹색-녹색이나 노랑-녹색과 같은 상태는 있을 수 없다는 것입니다. 이는 위에서 그래프로 표현한 소프트웨어의 구동 단계에서는 발생할 수 없음을 볼 수 있으며, 따라서 소프트웨어가 녹색-빨강의 초기 상태로 구동되는 한 안전함을 보일 수 있습니다.
이와 같은 정형 검증 기법은 인공지능 모델에 대해 적용하기는 여러 가지 어려움이 있습니다. 이는 인공지능 모델과 전통적인 소프트웨어의 구조 및 기능적 차이 때문으로, 먼저 인공지능 소프트웨어에 주어지는 입력이 전통적인 소프트웨어에 주어지는 입력에 반해 매우 복잡합니다. 앞서의 신호등 예시에서 소프트웨어에 주어지는 입력은 초기 상태뿐인 반면, 실제 인공지능 소프트웨어에서는 음성, 이미지, 텍스트 등 고차원의 입력이 주어집니다. 고차원의 입력에 따라 소프트웨어에 무수히 많은 상태들이 생겨날 수 있는 것이죠.
또 다른 어려움은 인공지능 소프트웨어가 작동하는 정확한 원리를 알기 어렵다는 점에서 기인합니다. 정형 검증 방법론을 적용하기 위해서는 주어진 소프트웨어를 수학적인 모델로서 표현해야 하는데, 여기에는 그 작동 원리를 파악하고 이에 따라 ‘압축’해 수학적인 모델을 설립하는 과정이 포함됩니다. 전통적인 소프트웨어는 한 줄 한 줄 실행되는 프로그램 형태를 띠고 있어 그 압축이 용이한 반면, 인공지능 모델은 복잡한 함수의 집합체로 표현되어 압축하는 것이 매우 어렵습니다.
▲고기혁 카이스트 사이버보안연구센터 AI보안팀장[사진=보안뉴스]
만약 이 모든 어려움을 해결하고 인공지능 소프트웨어의 안전성을 완벽하게 검증했다고 하더라도 실질적인 상황에서 활용 시 문제가 생길 수 있습니다. ‘직진 주행 중에는 차선을 벗어나지 않는다’는 안전성이 검증된 자율주행 자동차가, 응급 환자를 싣고 급히 달려가는 응급차를 위해 잠시 가던 길을 멈추고 살짝 틀어 길을 양보해주는 것이 가능하지 않을 것임은 뻔히 보이는 일입니다. 인공지능의 안전성 검증은 안전성 그 자체뿐만 아니라 실제 인공지능이 활용되는 상황을 면밀히 고려해야만 올바르게 해결할 수 있는 문제인 것입니다.
[글_ 고기혁 KAIST 사이버보안연구센터 AI보안팀장]
<저작권자: 보안뉴스(www.boannews.com) 무단전재-재배포금지>
원병철기자 기사보기
[2024-10-31] .jpg)
