基于改进军用安全模型的sJava语言

摘要

为了发现、控制软件中的非法信息流,利用改进后的军用安全模型对Java语言的安全性进行扩展,提出了一种基于类型的信息流控制方法。将安全级别编码为程序中的类型,并利用定型规则发现非法的信息流,扩展后的语言称为sJava。给出了sJava类型安全性的证明,实现了对开源的Java编译器Jikes的安全性改造。结果表明,sJava语言源程序能直接编译成字节码,不增加系统的运行负载。