title: 証明によるプログラムの信頼性の向上(仮)
author: Yasutaka Higa
cover:
lang: Japanese


# 研究目的(仮)

* 証明によるプログラムの信頼性の向上を目指す。
* 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。
* 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。

# 近況報告

* 運転手 for 坂井さん
* nkさんからGGJ のフィードバックが来ていたので wiki に反映
* OSの講義VMが攻撃を受けて学科ネットワークに影響
* いくつかの読み物


# VM が攻撃を受けた話

* kvm で起動していた受講生のVMが攻撃を受けた
* vagrant で作成したイメージを kvm で起動しっぱなしだった
* ネットワークはグローバルIPを使っていた
* セキュリティが甘い状態で攻撃を受けてしまい、学科ネットワークに影響が出た
* 現在は当該VMは shut off


# OSの講義と攻撃対策

* 今回は攻撃によるネットワーク異常が検出された
* シス管としてOSのVMの今後の攻撃対策をどうするのかと考えた時
* OSの講義のポリシが気になる
* シス管的には 後手 or 先手 の対策のどちらか？


# OS受講生側での対策

* 外部から攻撃されるのでVMのセキュリティはきっちりしましょう、と解説するスタンス
* セキュリティに関しては講義の一環なのでシス管は基本放置で異常検知からの対応のみ
* ただ、今回は学科ネットワークに影響が出た


# シス管として未然に防ぐ

* 攻撃は攻撃なので、未然に防ぐべき、というスタンス
* 例えば、OS受講者のVMは学内通信のみ、などkvm側で設定してしまう
* 講義的にセキュリティへの危機感ははあまり感じないかもしれない

# 読み物
* [Stricter Haskell](http://d.hatena.ne.jp/mkotha/20110509/1304947182)
* [Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何](http://togetter.com/li/634200)
* [定理証明系 Haskell](http://konn-san.com/prog/2013-advent-calendar.html)