Software is infrastructure: failures, successes, costs, and the case for formal verification

핵심 아이디어: 소프트웨어는 새로운 콘크리트다

우리의 도로, 다리, 발전소가 강철과 콘크리트가 아닌 보이지 않는 코드로 만들어진 세상을 상상해 보세요. 저자들은 소프트웨어가 현대 사회의 인프라(기반 시설)가 되었다고 주장합니다. 다리가 트럭을 버티지 못하고 무너지지 않아야 하는 것처럼, 병원, 은행, 비행기, 심지어 여러분의 토스터기까지 구동하는 우리의 소프트웨어도 완벽하게 작동해야 합니다.

이 논문은 단순하지만 무서운 질문을 던집니다: 만약 다리를 잘못된 수학으로 지었다면 무너질 것입니다. 그렇다면 소프트웨어를 잘못된 수학으로 만들었다면 어떤 일이 벌어질까요? 그 답은 이렇습니다. 수십억 달러가 사라지고, 사람들이 다치며, 때로는 사람들이 목숨을 잃습니다.

문제점: 우리는 모래 위에 성을 쌓고 있다

저자들은 우리가 소프트웨어를 물리적 공학과는 다르게 취급하고 있다는 점을 지적합니다.

• 벽 쌓기: 벽을 쌓으면 물리학이 테스트를 수행합니다. 벽이 너무 약하다면, 페인트를 칠하기도 전에 중력이 벽을 무너뜨릴 것입니다. 벽이 제대로 작동하는지 확인하기 위해 벽을 "실행"할 수는 없습니다. 그냥 만드는 것이고, 수학이 제대로 맞기를 바랄 뿐입니다.
• 소프트웨어 작성: 소프트웨어는 그저 텍스트일 뿐입니다. 버그를 직접 "느낄" 수는 없습니다. 코드가 제대로 작동하는지 보려면 실행해 봐야 합니다. 하지만 코드를 실행한다는 것은 낙하산이 펴지는지 확인하기 위해 자동차를 절벽 아래로 운전해 떨어뜨리는 것과 같습니다. 버그를 발견했을 때는 이미 충돌 사고가 발생한 후입니다.

논문은 재미있는 예를 듭니다. 만약 터미널에 rm -rf ~라고 입력하면, 여러분의 홈 폴더 전체가 삭제됩니다. 이것이 위험하다는 것을 알기 위해 실행해 볼 필요는 없습니다. 그저 매뉴얼(수학)을 읽어보면 무엇을 하는지 이해할 수 있습니다. 하지만 복잡한 코드의 경우, 매뉴얼을 읽는 것만으로는 충분하지 않습니다.

"잘못된 수학"의 대가: 1조 달러의 누수

논문은 지난 40년간 발생한 소프트웨어 실패 사례들을 '명예의 전당(Hall of Shame)'으로 나열하며, 실수가 얼마나 비싼 대가를 치르는지 보여줍니다. 이것들은 디지털 세계의 "다리 붕괴" 사건들입니다:

• 테라크-25 (의료): 버튼 두 개가 너무 빠르게 눌리는 현상 때문에 방사선 기계가 환자에게 과도한 양을 조사했습니다. 결과: 6명 사망.
• 런던 앰뷸런스 (응급 서비스): 새로운 배차 시스템에 메모리 누수(구멍 난 양동이 같은 현상)가 있었습니다. 데이터가 쌓여 시스템이 멈췄습니다. 결과: 구급차가 환자를 찾지 못했고, 20~30명이 사망했습니다.
• 보잉 737 MAX (항공): MCAS라는 소프트웨어 시스템이 단 하나의 결함 있는 센서를 바탕으로 비행기 코를 아래로 밀어버렸습니다. 결과: 두 차례의 추락 사고, 346명 사망, 200억 달러의 비용 발생.
• 호라이즌 스캔들 (금융): 잘못된 회계 시스템이 수천 명의 상인들에게 돈을 훔치고 있다고 알려주었습니다. 결과: 900명 이상의 사람들이 억울하게 투옥되었고, 시스템을 고치는 데 세금 10억 파운드 이상이 들었습니다.
• 크라우드스트라이크 (글로벌 IT): 아주 작은 업데이트 오류로 인해 전 세계 수백만 대의 컴퓨터가 파란 화면(블루스크린)과 함께 멈췄습니다. 결과: 전 세계적인 혼란과 수십억 달러의 사업 손실 발생.

저자들은 부실한 소프트웨어 품질이 미국 경제에 연간 1.56조 달러의 비용을 발생시킨다고 계산했습니다. 이는 많은 국가의 전체 GDP보다 큰 금액입니다. 이는 오로지 예방할 수 있었던 실수를 바로잡는 데 낭비되는 돈입니다.

해결책: "수학적 청사진"

논문은 우리가 추측하는 것을 멈추고, 소프트웨어를 실행하기 전에 그것이 작동함을 증명해야 한다고 주장합니다. 이것을 **형식 검증(Formal Verification)**이라고 부릅니다.

비유:
여러분이 마천루를 짓고 있다고 상상해 보세요.

• 현재 방식 (테스트): 100층을 짓고, 101층을 짓고, 102층을 짓습니다. 그리고 엘리베이터가 작동하는지 확인합니다. 만약 102층이 무너지면, 다시 허물고 다시 시도합니다. 이것은 비용이 많이 들고 위험합니다.
• 형식 검증: 콘크리트를 한 방울도 붓기 전에, 고급 수학을 사용하여 설계가 어떤 무게에서도 무너지지 않을 것임을 증명합니다. 설계도가 물리 법칙에 부합하는지 확인하여 완벽함을 보장합니다.

소프트웨어에서 이는 코드가 정확히 의도한 대로만 작동하고, 그 외의 일은 절대 하지 않음을 수학적으로 증명하는 것을 의미합니다.

정말 가치가 있을까? 네, 매우 남는 장사입니다

여러분은 "수학은 어렵고 비싸다. 그럴 가치가 있을까?"라고 생각할 수 있습니다. 논문은 네, 당연합니다라고 답합니다.

• **공기...