Provable non-interference between software of differing integrity levels

High integrity applications, such as those performing safety or security critical functions, are usually built to conform to standards such RTCA DO-178B or UK Def Stan 00-55. Typically such standards define ascending levels of criticality each of which requires a different and increasingly onerous level of verification. It is very common to find that real systems contain code of several different criticality levels. Unless segregation can be demonstrated to a very high degree of confidence, there is usually no alternative to verifying all the software components to the standard required by the most critical element, leading to an increase in overall cost. This paper describes the novel use of static analysis to provide a robust demonstration of the effective segregation of code of differing criticality levels, thus allowing appropriate verification techniques to be applied at the subprogram level.