컴파일러 검증 방법이 어떤것이 있을까요??

등으로 검색해 보시면 됩니다.

몇 가지 접근 방법이 있는데,

첫째는 컴파일러 자체를 만들 때 컴파일러에 오류가 없다는 것을 자체적으로 증명할 수 있도록 하는 고차원의 검증 능력을 갖춘 시스템으로 컴파일러를 작성하는 것입니다. 이론적으로 완벽한 이야기인데, 문제는 컴파일러라는 것의 덩치가 워낙에 클 수 있기 때문에 당장에 이런 컴파일러가 상용화되기는 힘들 것입니다. 또한 이 방법의 또 한 가지 한계는, 검증된 컴파일러 외에도 항상 많은 다른 컴파일러들이 존재할 수 있다는 것입니다. (아 물론 그 컴파일러를 작성하는 시스템은 또 어떻게 믿느냐는 문제가 계속 꼬리를 물기도 하고요.)

그래서 나온 생각이 컴파일러 자체는 오류가 있을 수 있을지도 모르지만, 컴파일러가 코드를 생성할 때 컴파일 과정에서 생성된 코드가 어떤 조건을 만족한다는 증명을 같이 생성하는 것입니다. 이 아이디어는 조지 네큘라가 시작한 것으로 proof carrying code 라고 불립니다. 컴파일러 전체는 증명하지 못할지라도 컴파일러가 어떤 증명을 자동으로 작성하게 하고, 그 자동으로 작성된 증명을 생성된 코드가 만족하는가를 검증하는 검증기를 만들면 됩니다. 이 검증기 자체는 컴파일러보다 작을 수 있기 때문에 믿어야 하는 소프트웨어의 크기 즉 trusted base 의 크기를 줄일 수 있으며, 서로 다른 컴파일러가 같은 형식의 증명 기술 방법을 사용하면 검증기를 공유할 수 있습니다. 하지만 이것도 아직은 실용화되려면 시간이 어느 정도 걸릴 것입니다.

마지막으로 이미 이용되고 있는 아이디어가 있는데 그것은 typed assembly language 라는 것입니다. 컴파일러가 생성하는 저급 언어 자체에 타입 시스템 등과 같은 고급 프로그래밍 언어의 방법론을 도입하거나 생성된 저급 언어에 대한 프로그램 분석을 통하여 최소한의 무결성을 검사하는 방법입니다. 컴파일러 자체의 무결성이나 정확성을 검사할 수는 없지만, 최소한 하드웨어나 플랫폼이 요구하는 최소한의 동작 방식을 따르고 있는지를 검사할 수는 있습니다. 자바 바이트 코드와 같은 것도 일종의 TAL이라고 볼 수 있으며, 실제로 자바 바이트 코드를 실행하기 전에 스택 언더플로 등과 같은 것은 정적으로 검사가 가능하지요.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin