Аннотация:
Рассматриваются программы, написанные на while-языке, с переменными двух типов безопасности: секретными и открытыми.
Статический анализ безопасности информационных потоков программ идентифицирует небезопасные информационные потоки, через которые могут произойти утечки информации.
При таком анализе по правилам, предложенным в [6], определяются типы конфиденциальности выражений, операторов и композиции операторов.
На основе этих правил был разработан алгоритм статического анализа безопасности программ, который заключается в попытке их типизирования. Если в результате программа типизируема, то она является безопасной с точки зрения информационных потоков; если же программе нельзя присвоить тип безопасности, то в ней содержатся небезопасные информационные потоки, и, следовательно, она является небезопасной.
С помощью средств генерации лексических и синтаксических анализаторов flex и bison [5] был разработан транслятор программ, написанных на while-языке, в код машины MMIX [2].