http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
- 中文 을 입력하시려면 zhongwen을 입력하시고 space를누르시면됩니다.
- 北京 을 입력하시려면 beijing을 입력하시고 space를 누르시면 됩니다.
RISS 인기검색어
- 검색키워드
- 저자 : 이광근(Kwangkeun Yi) (검색결과 71 건)
- 무료
- 기관 내 무료
- 유료
-
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.
-
-
-
이광근(Kwangkeun Yi),이욱세(Oukseh Lee),어현준(Hyunjun Eo),김정택(Jungtaek Kim),최응식(Woongsik Choi),류석영(Sukyoung Ryu),강현구(Hyun-Goo Kang),서선애(Sunae Seo),장성순(Sungsoon Jang),김범식(Bomshik Kim) 한국정보과학회 2001 한국정보과학회 학술발표논문집 Vol.28 No.2Ⅰ
상위의 타입 구조를 갖춘 (higher-order and typed) nML을 고안하고 그 컴파일러를 개발하였다. nML은 프로그래밍 언어 분야의 중요한 성과들을 충실히 실현한 언어로서, Standard ML과 Objective Caml의 장점과 실제 프로그래밍 세계의 관성을 염두에 두고 정의되었다. nML 컴파일러의 실용성과 안전성은 이미 여러 응용 시스템 소프트웨어의 개발로 실험되고 있다. 이 전통적인 컴파일러 시스템에 본 연구단의 프로그램 분석기술들이 장착되면서, 실시간 안전성 검증이 가능하고, 작고, 자발적인 적응력 있는 코드를 만들어내는 컴파일러로 발전하는 발판이 마련되었다.
-
-
이욱세(Oukseh Lee),이광근(Kwangkeun Yi) 한국정보과학회 1998 정보과학회논문지(B) Vol.25 No.8
Hindley/Milner 스타일의 복합형 타입 시스템(let-polymorphic type system)을 구현하는 타입 유추 알고리즘은 두 가지가 있다. 하나는 사실상 표준인 상향식(bottom-up) 알고리즘 W이고, 다른 하나는 하향식(top-down) 알고리즘 M이다. W 알고리즘은 안전성(soundness)과 완전성(completeness)이 수학적으로 검증되어 있고 가장 널리 쓰이기는 하지만, 타입 오류가 있는 입력 프로그램에 대해 때때로 모호한 메시지를 만들어 내는 문제점이 있다. 이에 M 알고리즘이 대안이 될 수 있는지를 확인할 필요가 있다. 하지만, 이 알고리즘은 단지 구현상에서 사용되었을 뿐, 정확하게 정의되어 있지 않고, 타입 시스템을 충실히 구현하는지(sound-and-completeness)도 증명되지 않았으며, W 알고리즘과 다른 점도 정확하게 규명되어 있지 않다. 본 논문에서는 M 알고리즘을 정확하게 기술하고, 복합형 타입 시스템을 충실히 구현함을 증명하며, 타입 오류가 있는 입력에 대해 W 알고리즘보다 신속히 타입 오류를 감지하는 성질을 증명한다. 본 논문에서의 증명은 실제 사용되었던 알고리즘에 대한 이론적인 검증인 것이다. The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard W algorithm that is bottom-up or context-insensitive and the other is a folklore algorithm that is top-down or context-sensitive. Because the latter algorithm has not been formally presented with its sound-and-completeness proofs and its relation with the W algorithm has not been rigorously investigated, its use in place of or in combination with W could not be seen appealing. In this paper, we formally define the context-sensitive, top-down type inference algorithm named M, prove its sound-and-completeness, and show a distinguishing property that M always stops earlier than W if the input program is ill-typed. Our proofs can be seen as theoretical justifications for various type-checking strategies in practice.
-
C 프로그램에서 소멸된 지역변수를 참조하는 오류를 정적으로 검출하기
이승중(Seungjung Lee),이광근(Kwangkeun Yi) 한국정보과학회 2011 한국정보과학회 학술발표논문집 Vol.38 No.2A
소멸된 지역변수 참조 오류란 C/C++로 작성된 프로그램에서 지역변수가 전역적인 포인터 변수에 의해 참조되어 지역변수의 범위를 벗어난 시점에 사용되는 것을 말한다. 이 오류는 언어 차원에서 강제할 방법이 없기 때문에 프로그래머가 부주의하면 쉽게 발생할 수 있고 프로그램의 의도되지 않은 실행을 일으키므로 오류를 미리 검출하는 것이 매우 중요하다. 프로그램의 구문분석만으로는 정상적인 경우와 오류인 상황을 구분할 수가 없기 때문에 의미구조 기반의 함수 간 분석을 필요로 한다. 함수 간 메모리 버퍼 오버런 분석기인 Airac[1]의 분석결과를 이용하여 소멸된 지역 변수 참조 오류를 검출할 수 있다. 이 분석기의 결과에 오류검출 알고리즘을 적용하여 오픈 소스 프로그램들에서 소멸된 지역변수 참조 오류를 얼마나 검출할 수 있는 지 실험해보았다.
-
Standard ML 프로그램의 실행 중 처리되지 않는 예외 상황을 예측하는 방법
류석영(Sukyoung Ryu),이광근(Kwangkeun Yi) 한국정보과학회 1996 한국정보과학회 학술발표논문집 Vol.23 No.2B
본 논문에서는 Standard ML(SML)[7, 6] 프로그램의 실행 중 처리되지 않는 예외 상황을 실행 전에 미리 예측하는 분석 방법을 제안한다. 이 분석 방법은 SML/NJ[2, 5] 컴파일러가 제공하는 타잎 정보를 이용하여 프로그램의 함수 흐름도를 먼저 예측하고, 이를 이용하여 예외 상황의 흐름을 방정식으로 표현한 후, 반복 부동점 방법으로 방정식을 풀어서 처리되지 않을 수 있는 예외 상황들을 예측한다. 이 방법의 속도는 현재 25 ~ 700 SML-lines/sec이고, 적절한 비용 대 성능비를 가지고 있는 것으로 밝혀졌다. 예를 들어, ML-Lex 프로그램을 분석하는데 약 23초가 걸렸고, 10개의 예외 상황 중에서 실제로 처리되지 않는 3개를 포함해서 4개의 예외 상황이 처리되지 않을 것으로 분석되었다. 이 분석으로 SML 프로그램의 갑작스런 중단을 미리 예측할 수 있으므로, SML 프로그램의 안전성을 한층 더 증가시킬 수 있다.
-
-
이욱세(Oukseh Lee),이광근(Kwangkeun Yi),김병철(Byungchul Kim),권경인(Kyoung-In Kwon) 한국정보과학회 1998 한국정보과학회 학술발표논문집 Vol.25 No.2Ⅰ
스택 머신 코드(stack-machine code)를 레지스터 기반 언어로 변환하는데 있어 스택의 타입 정보가 있으면 보다 효율적인 코드를 생성할 수 있음을 알아 내었다. 본 논문에서는 스택 머신 코드의 타입을 분석해야 할 이유를 제기하고, 요약해석 방법론에 따라 분석 방법을 제시하고, 제시된 분석 방법의 안전성을 짚어 본다.
ScienceON
DBpia연관 검색어 추천
이 검색어로 많이 본 자료
활용도 높은 자료
