組込みソフトウェア向けセキュリティチェック機能検証技術

摘要

組込みソフトウェアに関して，外部入力データに存在し得るセキュリティ脅威に対するチェック機能の実装漏れのリスクが課題であった。そこでC言語のコードを対象として，フォーマルメソッドと呼ばれるプログラムの数学的解析手法を活用して，外部入力データに対するセキュリティチェック機能の欠落や，同機能の誤使用を検出するツールを試作した。