Mercurial > hg > Members > atton > generated_seminar_slides

annotate slides/20140225/slide.md @ 49:be4bda2c5e58

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
auto-Update generated slides by script
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 28 Oct 2014 10:57:47 +0900
parents b841bf04be66
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
7
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
1 title: 証明によるプログラムの信頼性の向上(仮)
6
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 cover:
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
7
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
7 # 研究目的(仮)
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
8
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
9 * 証明によるプログラムの信頼性の向上を目指す。
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
10 * 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
11 * 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
12
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
13 # 近況報告
6
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
7
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
15 * 運転手 for 坂井さん
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
16 * nkさんからGGJ のフィードバックが来ていたので wiki に反映
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
17 * OSの講義VMが攻撃を受けて学科ネットワークに影響
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
18 * いくつかの読み物
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
19
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
20
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
21 # VM が攻撃を受けた話
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
22
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
23 * kvm で起動していた受講生のVMが攻撃を受けた
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
24 * vagrant で作成したイメージを kvm で起動しっぱなしだった
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
25 * ネットワークはグローバルIPを使っていた
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
26 * セキュリティが甘い状態で攻撃を受けてしまい、学科ネットワークに影響が出た
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
27 * 現在は当該VMは shut off
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
28
6
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
7
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
30 # OSの講義と攻撃対策
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
31
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
32 * 今回は攻撃によるネットワーク異常が検出された
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
33 * シス管としてOSのVMの今後の攻撃対策をどうするのかと考えた時
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
34 * OSの講義のポリシが気になる
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
35 * シス管的には 後手 or 先手 の対策のどちらか？
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
36
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
37
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
38 # OS受講生側での対策
6
ad44be90bafd auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
7
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
40 * 外部から攻撃されるのでVMのセキュリティはきっちりしましょう、と解説するスタンス
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
41 * セキュリティに関しては講義の一環なのでシス管は基本放置で異常検知からの対応のみ
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
42 * ただ、今回は学科ネットワークに影響が出た
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
43
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
44
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
45 # シス管として未然に防ぐ
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
46
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
47 * 攻撃は攻撃なので、未然に防ぐべき、というスタンス
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
48 * 例えば、OS受講者のVMは学内通信のみ、などkvm側で設定してしまう
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
49 * 講義的にセキュリティへの危機感ははあまり感じないかもしれない
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
50
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
51 # 読み物
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
52 * [Stricter Haskell](http://d.hatena.ne.jp/mkotha/20110509/1304947182)
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
53 * [Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何](http://togetter.com/li/634200)
b841bf04be66 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
54 * [定理証明系 Haskell](http://konn-san.com/prog/2013-advent-calendar.html)