열린 코드를 갖는 다단계 프로그램을 타입 정보로부터 자동으로 생성하기

정영범(Yungbum Jung),이원찬(Wonchan Lee),이광근(Kwangkeun Yi) 한국정보과학회 2011 한국정보과학회 학술발표논문집 Vol.38 No.1C

단계가 없는 고차원 프로그램(higher-order program)을 다단계 프로그램(multi-staged program)으로 타입의 도움을 받아 변환하는 방법을 제시한다. 이 방법은 최첨단의 다단계 프로그램 타입시스템에 기반했기에 직관적으로 이해가 쉽고, 열린 코드(open code)를 지원한다. 변환의 결과 나올 수 있는 열린 코드는 자유 변수(free variable)을 허용하여 나중에 사용자의 의도대로 자유롭게 묶이게 할 수 있다. 우리의 변환은 기존의 타입의 도움을 받아 특화시키는 Linger와 Sheard[2,3]의 방법에 비해 더 효율적이고, 더 많은 종류의 다단계 프로그램을 만들어 낼 수 있다.

함수 요약에 기반한 메모리 누수 정적 탐지기

정영범(Yungbum Jung),이광근(Kwangkeun Yi) 한국정보과학회 2009 정보과학회논문지 : 소프트웨어 및 응용 Vol.36 No.7

C프로그램에서 발생할 수 있는 메모리 누수(memory leaks)를 실행 전에 찾아 주는 분석기를 제안한다. 이 분석기는 SPEC2000 벤치마크 프로그램과 여러 오픈 소스 프로그램들에 적용시킨 결과 다른 분석기에 비해 상대적으로 뛰어난 성능을 보여준다. 총 1,777 KLOC의 프로그램에서 332개의 메모리 누수 오류를 찾아냈으며 이 때 발생한 허위 경보(false positive)는 47개에 불과하다(12.4%의 허위 경보율). 이 분석기는 초당 720 LOC를 분석한다. 각각의 함수들이 하는 일을 요약하여 그 함수들이 불려지는 곳에서 사용함으로써 모든 함수에 대해 단 한번의 분석만을 실행한다. 각각의 함수 요약(procedural summary)은 잘 매개화 되어 함수가 불려질 때의 상황에 맞게 적용할 수 있다. 실제 프로그램들에 적용하고 피드백 받는 방법을 통해 함수가 하는 일중에 메모리 누수를 찾는데 효과적인 정보들만으로 추리는 과정을 거쳤다. 분석은 요약 해석(abstract interpretation)에 기반하였기 때문에 C의 여러 문법 구조와 순환 호출(recursive call), 루프(loop)등은 고정점 연산(fixpoint iteration)을 통해 자연스럽게 해결한다. We present a static analyzer that detects memory leaks in C programs. It achieves relatively high accuracy at a relatively low cost on SPEC2000 benchmarks and several open-source software packages, demonstrating its practicality and competitive edge against other reported analyzers: for a set of benchmarks totaling 1,777 KLOCs, it found 332 bugs with 47 additional false positives (a 12.4% false-positive ratio), and the average analysis speed was 720 LOC/sec. We separately analyze each procedure's memory behavior into a summary that is used in analyzing its call sites. Each procedural summary is parameterized by the procedure's call context so that it can be instantiated at different call sites. What information to capture in each procedural summary has been carefully tuned so that the summary should not lose any common memory-leak-related behaviors in real-world C program. Because each procedure is summarized by conventional fixpoint iteration over the abstract semantics (`a la abstract interpretation), the analyzer naturally handles arbitrary call cycles from direct or indirect recursive calls.

열린 코드 다단계 프로그램의 타입 지향 자동 생성

정영범(Yungbum Jung),이원찬(Wonchan Lee),이광근(Kwangkeun Yi) 한국정보과학회 2012 정보과학회 컴퓨팅의 실제 논문지 Vol.18 No.3

단계가 없는 고차원 프로그램(higher-order program)을 다단계 프로그램(multi-staged program)으로 타입의 도움을 받아 변환하는 방법을 제시한다. 이 방법은 최첨단의 다단계 프로그램 타입시스템[1]에 기반했기에 직관적으로 이해가 쉽고, 열린 코드(open code)를 지원한다. 변환의 결과 나올 수 있는 열린 코드는 자유 변수(free variable)을 허용하여 나중에 사용자의 의도대로 자유롭게 묶이게 할 수 있다. 우리의 변환은 기존의 타입의 도움을 받아 특화시키는 Linger와 Sheard[2,3]의 방법에 비해 더 효율적이고, 더 많은 종류의 다단계 프로그램을 만들어 낼 수 있다. We present a type-directed transformation from unstaged higher-order programs into open code, multi-staged ones. Because our staging transformation is based on Kim et.al.'s type system [1] that supports open code, the resulting multi-staged programs can have code with free variables allowing intentional variable-capturing substitution. This means that our transformation system can generate more efficient staged program than the previous type-directed specialization techniques of Linger and Sheard [2,3].

아이락: C 프로그램의 메모리 오류 정적 분석기

정영범(Yungbum Jung),김재황(Jaehwang Kim),신재호(Jaeho Shin),이광근(Kwangkeun Yi) 한국정보과학회 2005 한국정보과학회 학술발표논문집 Vol.32 No.2

아이락(Airac)은 C 프로그램의 버퍼오버런(buffer overrun)오류를 찾아주는 정적 프로그램 분석기(static program analyzer)이다. 아이락은 요약해석(abstract interpretation)의 틀 속에서 디자인되었다. 설계 및 구현 과정에서 프로그램 분석 분야에서 축적되어온 다양한 기술들을 적용하여 분석의 성능 및 정확도 향상을 이룩하였다. 아이락은 리눅스 커널(linux kernel), GNU 소프트웨어, 상용 소프트웨어등에 적용되어 오류를 찾아냈다.

FuriosaAI 소프트웨어 스택 소개

정영범(YUNGBUM JUNG),구본철(BONCHEOL GU) 한국정보과학회 2021 정보과학회지 Vol.39 No.5

의미 기반 정적 분석과 규칙 명세 언어를 활용한 C/C++ 프로그램 보안 취약점 검출

윤용호(Yongho Yoon),진민식(Minsik Jin),정영범(Yungbum Jung),이규호(Gyuho Lee),김희동(Heedong Kim),김진국(Jingoog Kim) 한국정보과학회 2019 정보과학회 컴퓨팅의 실제 논문지 Vol.25 No.10

보안 취약점을 정적 분석으로 검출하는 것에는 여러 장점이 있지만 일반적으로 새로운 취약점 검출을 지원하기 위한 비용이 크다는 어려움이 있다. 검출 범위를 손쉽게 확장하기 위해 보안 취약점을 표현할 수 있는 방법을 정의하고 그 표현에 부합하는 프로그램을 검출하는 기술이 존재하지만 대개 프로그램의 모양에만 의존하거나 간단한 값 흐름 분석에만 적용할 수 있었다. 이런 점을 보완하기 위하여 보안 약점을 표현할 수 있는 규칙 명세 언어를 정의하고 이를 기반으로 취약점을 검출하는 요약 해석 기반 정적 분석 도구를 고안 및 구현하였다. 분석 대상 언어는 C/C++이며, 상용 정적 분석 도구에 포함된 C/C++ 분석 엔진을 기반으로 규칙 명세 언어 매칭 검사기를 구현했다. 대상 취약점은 CWE(Common Weakness Enumeration) 목록 중 적합한 17가지를 선별했다. 정오탐률 계산을 위해 자동생성한 테스트 셋을 대상으로 성능을 시험한 결과 정탐률은 61.4%, 오탐률은 7.5%로 집계되었다. In spite of a number of advantages to detecting security holes using static semantic analysis, new types of vulnerabilities are not easily detected by the existing static analyzers. Some technologies have defined mechanisms to identify security vulnerabilities and match them with the programs but they are based only on simple syntactic analysis or data-flow analysis. We defined rule description language (RDL) to describe vulnerability rules and made a static analyzer based on abstract interpretation that detects the denoted defects in C/C++ programs. Implementation of the RDL matching engine was based on an existing commercial C/C++ static analysis tool. We selected 17 rules from the CWE (Common Weakness Enumeration) list that fit with RDL and static analysis. We evaluated the correctness of our tool with automatically generated test cases and the result showed 61.4% true positive and 7.5% false negative rates.

C 프로그램의 버퍼 오버런(buffer overrun) 오류를 찾아 주는 정적 분석기의 설계와 구현

이광근(Kwangkeun Yi),김재황(Jaewhang Kim),정영범(Yungbum Jung) 한국정보과학회 2006 정보과학회논문지 : 소프트웨어 및 응용 Vol.33 No.5

이 논문에서는 정적 프로그램 분석(static program analysis)과 통계적 분석(statistical analysis)의 조합을 가지고 실제적인 C 프로그램을 검증한 경험을 보고한다. 정적 분석과 통계적 분석의 조합은 입력 프로그램에 제한을 두지 않는 정적 분석기에서 발생하는 불가피한 허위 경보를 줄이기 위한 것이다. 우리는 ANSI C 프로그램이 실행 중에 겪을 수 있는 모든 배열 참조 오류(buffer overrun)를 찾아주는 정적 프로그램 분석기 아이락(Airac, Array Index Range Analyzer for C)을 고안하고 구현하였다. 분석의 안전성(soundness)을 유지하면서 프로그램 분석 분야에서 오랫동안 축적된 기술들을 활용하여 분석 비용 절감 및 정확도 향상을 달성했다. 대상 프로그램에 제한을 두지 않는 안전한 분석은 정확도에 한계가 있으므로 불가피한 허위 경보가 존재할 수 있다. 이러한 허위 경보(예를 들어 530만 줄짜리 상용 C 프로그램에 대한 분석 결과 아이락은 970개의 배열 참조 오류 경보를 발생시켰으나 그 중 737개는 허위 경보였다.)에 대처하기 위해 우리는 통계적 사후 분석을 시도하였다. 통계적 사후 분석은 주어진 경보가 실제 오류를 가리킬 확률을 계산한다. 이렇게 계산된 확률은 두 가지 방법으로 사용된다. 1) 경보를 걸러내거나, 2) 실제 오류에 대한 경보일 가능성이 높은 것들을 우선적으로 사용자에게 보여준다. 우리는 리눅스 커널 프로그램과 알고리즘 교과서의 프로그램들을 대상으로 실험을 수행했다. 우리 실험에서 실제 오류를 놓칠 위험이 허위 경보의 위험의 3배라고 설정한 경우 74.83%의 허위 경보를 걸러낼 수 있었고, 참일 확률이 높은 경보부터 검증하는 경우 15.17%의 허위 경보만이 실제 오류 50%와 섞여 있었다. We present our experience of combining, in a realistic setting, a static analyzer with a statistical analysis. This combination is in order to reduce the inevitable false alarms from a domain-unaware static analyzer. Our analyzer named Airac(Array Index Range Analyzer for C) collects all the true buffer-overrun points in ANSI C programs. The soundness is maintained, and the analysis' cost-accuracy improvement is achieved by techniques that static analysis community has long accumulated. For still inevitable false alarms (e.g. Airac raised 970 buffer-overrun alarms in commercial C programs of 5.3 million lines and 737 among the 970 alarms were false), which are always apt for particular C programs, we use a statistical post analysis. The statistical analysis, given the analysis results (alarms), sifts out probable false alarms and prioritizes true alarms. It estimates the probability of each alarm being true. The probabilities are used in two ways: 1) only the alarms that have true-alarm probabilities higher than a threshold are reported to the user; 2) the alarms are sorted by the probability before reporting, so that the user can check highly probable errors first. In our experiments with Linux kernel sources, if we set the risk of missing true error is about 3 times greater than false alarming, 74.83% of false alarms could be filtered; only 15.17% of false alarms were mixed up until the user observes 50% of the true alarms.

OWASP 벤치마크의 보안약점 탐지 점수를 높이기 위한 정적 분석 기술

강동옥(Dongok Kang),김경환(Kyoung-Hwan Kim),진민식(Minsik Jin),정영범(Yungbum Jung) 한국정보과학회 2016 정보과학회지 Vol.34 No.3