자동 프로그램 수정과 패치 적합성 검증
이 연구 주제는 소프트웨어 결함을 자동으로 수정하는 프로그램 수리(automated program repair) 기술과, 생성된 패치가 실제로 올바른지 판단하는 검증 기술을 함께 다룬다. 연구실은 단순히 테스트를 통과하는 그럴듯한 패치를 많이 만드는 것에 그치지 않고, 실제 의도된 동작을 만족하는 고신뢰 패치를 선별하는 문제를 핵심 과제로 본다. 이는 자동 수리 분야에서 잘 알려진 오버피팅 패치 문제를 해결하기 위한 방향으로, 소프트웨어 품질과 유지보수 생산성을 동시에 높이는 데 목적이 있다. 구체적으로는 테스트 기반 프로그램 수정, 결함 위치 식별, 제약 조건 기반 패치 생성, 기호 실행, MaxSMT 기반 최소 수정 탐색 등 다양한 정형적·탐색적 기법을 결합한다. 연구실의 대표 성과로는 preservation condition을 활용해 패치의 적합성을 반자동으로 분류하는 방법, 제약 조건과 탐색 기법을 활용한 프로그램 수정 특허, 그리고 자동 생성된 패치의 기능적 안정성을 검증하는 기술이 있다. 이러한 접근은 단순한 버그 수정 자동화를 넘어, 생성 결과를 신뢰할 수 있는 수준으로 끌어올리는 데 강점을 가진다. 이 연구는 산업 현장에서의 디버깅 자동화, 유지보수 비용 절감, 대규모 코드베이스 관리, 그리고 안전성이 중요한 시스템의 품질 보증에 직접 연결된다. 특히 여러 정부·산학 프로젝트를 통해 실용 도구화 가능성이 높게 검증되고 있으며, 향후에는 대규모 언어모델과의 결합을 통해 패치 생성 효율을 높이되, 정형 검증과 테스트 기반 확인을 함께 적용하는 하이브리드 자동 수정 체계로 발전할 가능성이 크다.
프로그램 명세, 변경 계약, 형식 검증
이 연구 주제는 프로그램의 의도된 동작과 변경 사항을 명시적으로 기술하고, 그 명세를 바탕으로 소프트웨어의 정확성을 검증하는 데 초점을 둔다. 연구실은 소프트웨어 오류의 상당수가 기존 코드에 대한 잘못된 변경에서 비롯된다는 점에 주목하여, 전체 프로그램 계약이 아니라 변경된 부분의 기대 동작을 중심으로 표현하는 변경 계약(change contracts) 개념을 발전시켜 왔다. 이는 유지보수와 진화 과정에서 실제 개발자가 마주하는 문제를 더 직접적으로 다룰 수 있는 명세 방식이다. 방법론적으로는 JML과 같은 명세 언어, 동적 검사기와 정적 검사기, 의미론 정의, 회귀 오류 탐지, 버그 위치 추적, 테스트 실패 원인 분류 등의 기술이 핵심을 이룬다. 연구실은 변경 계약의 형식적 의미를 정립하고, 이를 바탕으로 프로그램이 명세된 방식대로 수정되었는지 확인하는 도구적 기반을 구축해 왔다. 이러한 연구는 단순한 정적 분석을 넘어, 테스트 생성 지원과 디버깅 보조까지 연결되며, 소프트웨어 품질 관리의 이론과 실무를 잇는 다리 역할을 한다. 이 주제의 학술적 의의는 소프트웨어 공학에서 명세와 검증의 활용 장벽을 낮추면서도 실질적인 유지보수 문제를 해결할 수 있다는 데 있다. 앞으로는 레거시 코드 분석, 저코드/로우코드 환경, 생성형 AI가 만든 코드의 행위 보증 등 새로운 개발 패러다임에서도 변경 의도를 엄밀하게 표현하고 검증하는 기술이 더욱 중요해질 것이다. 연구실의 축적된 명세·검증 연구는 신뢰 가능한 자동화 소프트웨어 개발 환경 구축에 핵심 기반이 된다.
소프트웨어 테스팅, 퍼즈 테스팅, 보안 취약점 패치
이 연구 주제는 소프트웨어 테스팅과 자동 수리를 긴밀하게 결합하여, 버그와 보안 취약점을 더 빠르고 정확하게 찾아내고 수정하는 기술을 다룬다. 연구실은 특히 퍼즈 테스팅을 단순한 결함 탐지 도구로만 보지 않고, 자동 프로그램 수리 결과를 평가하고 강화하는 상호보완적 기술로 바라본다. 이를 통해 제로데이 공격이나 공급망 환경에서 발견되는 취약점에 대해 탐지와 수정이 분리되지 않은 통합 대응 체계를 지향한다. 대표적으로 퍼즈 입력을 활용한 패치 검증, 취약점 자동 패칭, 바이너리 기반 최소 보안 패치 생성, 메모리 누수와 같은 비기능 결함의 선제적 수정 기술이 포함된다. 단일 페이지 웹 애플리케이션의 메모리 누수를 사후 탐지가 아니라 사전적·패턴 기반 수리로 다루는 연구는, 실제 오픈소스 프로젝트에 적용 가능한 수준의 실효성을 보여준다. 또한 SW 공급망 환경에서 역공학의 불완전성을 극복하면서도 보안성과 안전성을 만족하는 마이크로 패치 기술 개발은, 실전형 사이버 보안 대응과 밀접하게 연결된다. 이 분야의 파급효과는 매우 크다. 최신 소프트웨어는 배포 주기가 짧고 의존 라이브러리가 복잡해 취약점 대응 속도와 정확도가 경쟁력으로 직결되기 때문이다. 연구실의 접근은 테스트, 퍼징, 자동 수리, 보안 검증을 하나의 연속된 공정으로 통합함으로써, 개발자 부담을 줄이면서도 패치의 실용성과 신뢰성을 동시에 확보하려는 방향을 제시한다. 향후에는 대규모 언어모델 기반 코드 이해 기술과 결합해, 더 넓은 범위의 취약점과 실행 환경에 적용 가능한 지능형 보안 패치 플랫폼으로 확장될 수 있다.