Proof-Carrying Code (PCC) is a convincing technology for certifying the safety of mobile code, yet how to generate the safety proof is a matter for investigation. The existing proof construction either assumes that the programmer provides the program invariants, or is limited to a class of properties that are inferable by the type system technology.
In this thesis, we propose a program proof construction, which does not require programmer provided invariants, and generates proofs for wider class of properties than types. Our proposal is to combine abstract interpretation and Hoare logic. Our proof construction algorithm generates a Hoare proof of a program from its abstract interpretation results. Abstract interpretation makes the invariant generation automatic and allows wider class of properties applicable to PCC. Hoare logic makes the program proofs general enough to be checkable by common code consumers who do not know which analysis technique has been used to generate the proof. From abstract interpretation, our proof construction algorithm defines a systematic way to construct Hoare proofs using the concretization formula of the abstract values and the prescribed soundness of the abstract operators.
One problem in our automatic proof construction is that abstract interpretation results are often unnecessarily informative for intended Hoare proofs. An abstract interpreter is usually designed to compute program invariants that are as strong as possible, while the program proofs are intended to show the satisfaction of a particular property of a program.
To handle this over-informative invariants, we propose a framework for designing algorithms called ${\em abstract-value slicers}$, that filter out unnecessary invariants from abstract interpretation results. Given a property of interest and the invariants generated by an abstract interpreter, abstract-value slicer collects the invariants that are related to the verification of the property. Abstract-value slicer uses a special domain called ${\em extractor domain}$ and backward extractor transformers for atomic terms. An extractor domain specifies the level of information exposure in the abstract domain. The framework provides a generic abstract-value slicer that can be instantiated into a slicer for a particular abstract interpretation. In the thesis, we present methods to construct correct parameters for the generic abstract-value slicer. The methods allow construction of accurate and efficient abstract-value slicers. We also consider abstract-value slicers for systematically-constructed abstract interpretations.
We implemented an abstract-value slicer and the proof construction algorithm for an existing relational analysis and applied it on array-accessing programs. In this experiment, the abstract-value slicer identified 62% - 81% of the invariants as unnecessary, which resulted in 52% - 84% reduction in the size of program proofs.
증명보내기 (PCC: Proof-carrying Code) 방법은 네트웍에서 돌아다니는 코드의 안전성을 보장할 수 있는 잘 알려진 기법이나, 코드의 안전성을 만드는 방법에 관해서는 아직 충분한 연구가 이루어지지 않았다. 안전성 증명을 만드는 기존의 방법들은 프로그래머가 증명을 위한 조건을 알아서 제시한다고 가정하거나, 타입 시스템에서 제공되는 특징에 관련된 증명만을 코드의 안전성 증명으로 간주하고 있다.
이러한 기존의 코드의 안전성 증명 생성 방법에 관한 문제를 해결하고자, 우리는 프로그래머가 조건을 제시할 필요도 없고, 타입 이외의 프로그램 성질에 관해서도 안전성 증명을 생성할 수 있는 프로그램 증명 알고리즘을 제안한다. 우리 연구에서 제시하는 방법은 기존에 잘 알려진 두가지 기법을 사용하는데, 그것은 요약해석(Abstract Interpretation) 과 호어증명 기법 (Hoare Logic) 이다. 이 논문에서 제안하는 증명 생성 알고리즘은 요약해석으로부터 생성된 프로그램의 분석 결과를 호어증명기법을 이용하여 호어 증명으로 바꾼다. 자동으로 프로그램 분석을 수행하는 요약해석 기법은 타입보다 더 일반적인 성질을 유추할 수 있다. 더불어, 코드의 안전성 증명으로 사용하는 호어 증명은 일반적인 코드 사용자가 기본적인 로직과 호어증명 기법에 대해서 알기만 하면 제공된 증명이 안전한지 손쉽게 검사할 수 있는 장점이 있다. 이것은 코드 생성자가 어떤 분석 기법을 사용하여 코드 안전성을 확보했는지 코드 사용자가 꼭 알아야 하는 기존의 증명보내기 기법에 비해서 훨씬 넓은 범위에서 적용가능하다.
하지만, 이 논문에서 제안된 코드 안전성 증명 생성 방법은 한가지 큰 문제점을 가지고 있다. 그것은 요약해석이 만들어내는 프로그램 분석 결과가 우리가 증명하길 원하는 성질 이외에 더 많은 성질들에 관해서 계산하기 때문에, 호어 증명으로 만들었을 때 너무 큰 증명이 생성된다는 사실이다. 일반적으로, 코드의 안전성에 관해서 이야기 할 때, 우리는 한가지 사실에 관해서 언급하기 마련인데 비해서, 요약해석은 가능한 모든 사실에 관해서 분석을 수행하기 때문에 이같은 문제가 발생한다.
요약해석이 우리의 필요에 비해서 너무 자세한 분석 결과를 내는 문제를 해결하기 위해서, 우리는 요약값자르기 (Abstract-value Slicing) 라는 새로운 방법을 고안하고, 그것을 일반화한 프레임워크를 함께 제안한다. 요약값자르기 방법은 요약해석의 분석 결과를 살펴보고, 불필요한 정보를 없애는 기법이다. 즉, 증명하고자 하는 성질이 주어지고, 요약해석이 분석 결과를 계산하면, 요약값자르기는 요약해석이 준 분석 결과로부터 주어진 성질과 관계없는 정보를 없앤다. 우리는 요약값자르기 기법을 일반화된 프레임워크로 제안하여, 다양한 요약해석 분석기에 어울리는 요약값자르기 알고리즘이 정의되도록 하였다. 요약값자르기 알고리즘을 조건에 따라 정의하려면 함께 제시해야 하는 매개 변수들이 있는데, 이 연구에서는 그런 매개 변수들을 적절하게 정의하는 방법론에 관해서도 기술하고 있다.
마지막으로, 우리가 제안하는 방법들을 모두 ML 로 구현하여 실험을 수행했다. 우선, 잘알려진 관계형 (relational) 요약해석 알고리즘을 구현하였고, 그 분석 결과를 적절히 잘라내는 요약값자르기 알고리즘도 구현을 하였다. 그리고, 분석 결과로부터 호어 증명 트리를 생성하는 자동 증명 생성 함수도 구현을 하여, 배열을 사용하는 몇 개의 프로그램에 적용하여 보았다. 실험 결과, 우리의 요약값자르기 기법이 62% 에서 81% 의 요약해석의 분석 결과가 불필요하다고 판단을 하였고, 불필요한 분석 결과를 제외하고 호어 증명 트리를 세웠을 때, 52% 에서 84% 정도 크기가 줄어드는 것을 확인할 수 있었다.
