A Methodology for Evaluating Languages and their Compilers for Secure Applications.

摘要

This technical memorandum proposes a methodology for the evaluation of Higher Order Programming Languages and their compilers that are to be used in the development of trusted software for secure application. The basic language issues identified are portable software, storage management, input-output, and exceptional conditions and handling. Two general techniques for resolving these issues are identified: (1) avoidance techniques whereby a language design avoids the issue, and (2) automatic techniques in which the compiler or its run system help resolve the issue. The automatic techniques fall into three categories: (1) confinement techniques, which prevent a program from employing its underlying machine in such a way that the machine would not legally implement the language; (2) predictive techniques, which infer some property of a program before it runs on any input data, and (3) automated debugging techniques, such as test data generation and debugging output. The report concludes with the use of the evaluation criteria on three language implementations, PL/1, Algol 68, and Pascal, for their resolution of the storage management issue. (Author)