(An) explicit polymorphic type system for verifying untrusted low-level codes

Abstract

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.