セキュアコーディング(法政大学 理工学部 応用情報工学科 2年次後期 (2011年度))
授業の到達目標
バグやセキュリティホールのない安全なソフトウェアを設計する手法として近年重要度を増しているフォーマルメソッド（形式手法・数理的技法）について学び，その基本的な考え方を習得することを目標とする．
授業の概要と方法
安全なソフトウェアの設計に数理論理学が必須のツールであることを動機付けた後，数理論理学の基本概念（構文論と意味論，命題論理，述語論理，健全性，完全性）とそのソフトウェア設計への応用（構成的論理，様相論理，ホーア論理などを用いたアプローチ）を学ぶ．さらに，フォーマルメソッドの最近の研究事例を紹介し，今後の展望を与える．
数学的な面白さと，エンジニアリングとしての重要性の，両方が感じられるような授業を目指したい．数学的証明の詳細まで深入りして解説することはしないが，最も重要な「論理的に厳密に考える姿勢」が習得できるような授業を心掛けたい．基本的には講義形式にて授業を行う．
授業計画
(進行状況にあわせて適宜修正します. 資料はなるべく授業の前日までにアップするようにしますが, 間に合わなかったらすみません. また, 資料にアクセスする際にパスワードを要求されることがあります.)
- 第1回(9/23) 数理論理学を学ぶということ〜数学基礎論からフォーマルメソッドまで [資料]
- 第2回(9/30) 命題論理〜構文論・意味論・健全性 [資料]
- 第3回(10/7) 述語論理〜完全性定理 [資料]
- 第4回(10/14) 計算（不）可能性 [資料]
- 第5回(10/21) 計算（不）可能性のさまざまな階層〜算術的階層から多項式時間階層まで [資料]
- 第6回(10/28) 不完全性定理 [資料]
- (11/4) 休講
- 第7回(11/11) さまざまな独立命題〜ヒドラ-ヘラクレス戦 [資料]
- 第8回(11/18) 構成的論理 [資料]
- 第9回(11/25) ラムダ計算 [資料]
- 第10回(12/2) 型つきラムダ計算とカリー・ハワード対応 [資料]
- 第11回(12/9) 定理証明支援系Coqのデモ・演習 [資料]
- 第12回(12/16) ホーア論理 [資料]
- 第13回(12/23) 様相論理とモデル検査 [資料]
- 第14回(1/13) ホットトピックス（匿名性・プライバシの形式検証） [資料]
- 試験（まとめ・評価）
テキスト
講義資料を配布する．
授業外に行うべき学習活動（準備学習等）
事前にテキスト（配布する講義資料）に目を通し，講義終了後に復習することが望ましい．特に，講義中の小テストにおいて出題される問題の一部は，期末試験にも形を変えて出題される可能性があり，十分に復習しておきたい．また，本授業内容に興味を抱き，数理論理学とその応用についてより深く学びたいという意欲のある者は，以下に挙げる参考書「論理と計算のしくみ」(萩谷昌己・西崎真也)を並行して熟読することをすすめる．
参考書
-
萩谷昌己・西崎真也: 論理と計算のしくみ. 岩波書店 (2007).
ISBN 978-4-00-006191-9
(本授業は全般にわたりこの優れた教科書をベースにしています)
-
鹿島亮: 数理論理学. 朝倉書店 (2009).
(証明までふくめて論理学をきちんと学びたい人にぜひおすすめします)
-
新井敏康: 数学基礎論. 岩波書店 (2011).
(やや高度な内容を含みますが本格的に学びたい人はぜひトライしてください)
-
田中一之・鹿島亮・角田法也・菊池誠: 数学基礎論講義. 日本評論社 (1997).
(第7回授業はこの教科書を大いに参考にしています)
-
高橋正子: 計算論. 近代科学社 (1991).
(第9回授業の内容を深く理解したい人にぜひ一読をおすすめします)
-
林晋: プログラム検証論. 共立出版 (1995).
(第12回授業はこの教科書を大いに参考にしています)
-
林晋・八杉満利子訳・解説: ゲーデル不完全性定理(岩波文庫). 岩波書店 (2006).
(ゲーデルに興味をもった人におすすめします)
-
ダグラス・ホフスタッター: ゲーデル，エッシャー，バッハ―あるいは不思議の環
20周年記念版. 野崎昭弘・柳瀬尚紀・はやしはじめ訳. 白揚社 (2005).
(人工知能(AI)に関心のある人におすすめします)
-
結城浩: 数学ガール／ゲーデルの不完全性定理. ソフトバンククリエイティブ (2009).
(話題の本です)
-
池渕未来:
プログラミングCoq 〜絶対にバグのないプログラムの書き方〜.
(第11回授業に興味を持った人はこのチュートリアルで大いに手を動かしましょう)
-
特集 フォーマルメソッドの新潮流.
情報処理, Vol.49, No.5, pp.491--543 (2008).
[CiNii]
(産業界での応用についても書かれています)
-
萩谷昌己, 塚田恭章 (編): 数理的技法による情報セキュリティ.
日本応用数理学会監修, シリーズ応用数理, 第1巻, 共立出版 (2010).
(フォーマルメソッドと暗号理論の融合に関する最近の話題を紹介しています)
成績評価基準
期末試験により評価する．ただし，講義中の小テストの結果も考慮する．
情報機器使用
第11回授業では，PC に定理証明支援系 Coq をインストールして使用する．
現時点での最新バージョン Coq 8.3（に CoqIDE と呼ばれるインターフェースがバンドルされたもの）のバイナリは次の URL からダウンロード可能である．
その他
必須ではないが，科目「集合と命題論理」「離散数学」を履修していることが望ましい．また，「データ構造とアルゴリズム」「ソフトウエア工学」「人工知能概論」「形式言語とオートマトン」「論理回路」「数論」「計算量の理論」等の科目と関連が深い．
塚田恭章