The verification of an untrusted code becomes an important issue in recent days, both in the mobile computing environment and in the safety-critical software systems. The code attached with the incoming mail or an external code running in the web-browser is common in these days.
A verification mechanism for the low-level code property is important. The code provider generates the low-level code and the code consumer needs to check the property of the low-level code. The decent compiler system guarantees the safety of the source code, but there is no good mechanism for the intermediate languages or the low-level languages.
We design an intermediate language, etySECK, which is low level enough to reduce the repeated compilation overheads, but high level enough to facilitate the verification of the code property. We present a type system with effect extension as a verification mechanism and then prove the soundness of our system.
검증되지 않은 코드의 안전성의 검증은 최근에 와서 인터넷이나 모발컴퓨팅 환경등에서 그리고, 소프트웨어의 안전성이 아주 중요한 시스템에서 중요한 문제가 되고 있다. 전자우편에 첨부되어오는 코드를 수행하거나 웹브라우져가 외부로 부터 코드를 받아서 수행하는 일등은 일상 생활에서 자주 발생한다.
이런 환경에서 목적코드에 가까운 저 수준 언어의 성질에 관한 검증방법이 절실히 요구되고 있다. 목적코드를 만들어 내는 쪽에서는 고급언어로 부터 목적언어를 만들어 내면 되지만, 이 목적코드를 사용하는 코드 소비자입장에서는 목적언어에 대한 검증을 할 수 있는 방법이 필요하게 된다. 잘 만들어진 컴파일러 시스템은 소스언어의 안전성을 검증할 수 있는 방법을 제공하지만, 중간언어나 목적어 코드에 대해서는 이런 일이 되어 있지 않다.
이 논문에서는 매번 다시 컴파일 하는 비용을 줄일 수 있고, 코드의 안전성 검증이 가능하도록 하기 위해, 중간언어인 etySECK를 정의 한다. 이를 바탕으로 실제검증이 가능하도록 타입시스템을 설계하고, 이의 안전성에 관한 증명을 한다.
