Mercurial > hg > Members > atton > generated_seminar_slides

--- a/slides/20140225/slide.html	Tue Feb 25 14:22:39 2014 +0900
+++ b/slides/20140225/slide.html	Tue Feb 25 15:57:58 2014 +0900
@@ -2,7 +2,7 @@

 <html lang="Japanese">
 <head>
-	<title>title</title>
+	<title>証明によるプログラムの信頼性の向上(仮)</title>
 	<meta charset="UTF-8">
 	<meta name="viewport" content="width=1274, user-scalable=no">
 	<meta name="generator" content="Slide Show (S9)">
@@ -18,13 +18,13 @@
 </head>
 <body class="list">
 	<header class="caption">
-		<h1>title</h1>
+		<h1>証明によるプログラムの信頼性の向上(仮)</h1>
 		<p>Yasutaka Higa</p>
 	</header>
 	<div class="slide bg" id="Cover"><div>
 		<section>
 			<header>
-				<h2>title</h2>
+				<h2>証明によるプログラムの信頼性の向上(仮)</h2>
 			</header>

 			<img src="pictures/" alt="">
@@ -38,12 +38,12 @@
 <div class="slide" id="2"><div>
 		<section>
 			<header>
-				<h1 id="hoge">hoge</h1>
+				<h1 id="section">研究目的(仮)</h1>
 			</header>
 			<!-- === begin markdown block ===

       generated by markdown 1.1.1 on Ruby 2.1.1 (2014-02-24) [x86_64-darwin12.0]
-                on 2014-02-25 14:22:36 +0900 with Markdown engine kramdown (1.3.2)
+                on 2014-02-25 15:57:21 +0900 with Markdown engine kramdown (1.3.2)
                   using options {}
   -->

@@ -51,8 +51,9 @@


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


@@ -63,14 +64,113 @@
 <div class="slide" id="3"><div>
 		<section>
 			<header>
-				<h1 id="fuga">fuga</h1>
+				<h1 id="section-1">近況報告</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+
+<ul>
+  <li>運転手 for 坂井さん</li>
+  <li>nkさんからGGJ のフィードバックが来ていたので wiki に反映</li>
+  <li>OSの講義VMが攻撃を受けて学科ネットワークに影響</li>
+  <li>いくつかの読み物</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="4"><div>
+		<section>
+			<header>
+				<h1 id="vm-">VM が攻撃を受けた話</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+
+<ul>
+  <li>kvm で起動していた受講生のVMが攻撃を受けた</li>
+  <li>vagrant で作成したイメージを kvm で起動しっぱなしだった</li>
+  <li>ネットワークはグローバルIPを使っていた</li>
+  <li>セキュリティが甘い状態で攻撃を受けてしまい、学科ネットワークに影響が出た</li>
+  <li>現在は当該VMは shut off</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="5"><div>
+		<section>
+			<header>
+				<h1 id="os">OSの講義と攻撃対策</h1>
 			</header>
 			<!-- _S9SLIDE_ -->


 <ul>
-  <li>fugaaa</li>
-  <li>fugafuga</li>
+  <li>今回は攻撃によるネットワーク異常が検出された</li>
+  <li>シス管としてOSのVMの今後の攻撃対策をどうするのかと考えた時</li>
+  <li>OSの講義のポリシが気になる</li>
+  <li>シス管的には 後手 or 先手 の対策のどちらか？</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="6"><div>
+		<section>
+			<header>
+				<h1 id="os-1">OS受講生側での対策</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+
+<ul>
+  <li>外部から攻撃されるのでVMのセキュリティはきっちりしましょう、と解説するスタンス</li>
+  <li>セキュリティに関しては講義の一環なのでシス管は基本放置で異常検知からの対応のみ</li>
+  <li>ただ、今回は学科ネットワークに影響が出た</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="7"><div>
+		<section>
+			<header>
+				<h1 id="section-2">シス管として未然に防ぐ</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+
+<ul>
+  <li>攻撃は攻撃なので、未然に防ぐべき、というスタンス</li>
+  <li>例えば、OS受講者のVMは学内通信のみ、などkvm側で設定してしまう</li>
+  <li>講義的にセキュリティへの危機感ははあまり感じないかもしれない</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="8"><div>
+		<section>
+			<header>
+				<h1 id="section-3">読み物</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li><a href="http://d.hatena.ne.jp/mkotha/20110509/1304947182">Stricter Haskell</a></li>
+  <li><a href="http://togetter.com/li/634200">Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何</a></li>
+  <li><a href="http://konn-san.com/prog/2013-advent-calendar.html">定理証明系 Haskell</a></li>
 </ul>
 <!-- === end markdown block === -->
--- a/slides/20140225/slide.md	Tue Feb 25 14:22:39 2014 +0900
+++ b/slides/20140225/slide.md	Tue Feb 25 15:57:58 2014 +0900
@@ -1,15 +1,54 @@
-title: title
+title: 証明によるプログラムの信頼性の向上(仮)
 author: Yasutaka Higa
 cover:
 lang: Japanese


-# hoge
+# 研究目的(仮)
+
+* 証明によるプログラムの信頼性の向上を目指す。
+* 信頼性とは、プログラムがプログラマの予期しない動作をしないことである。
+* 目標の例としては、現在は実行時にしか検出できないエラーなどを実行以前に検出することがある。
+
+# 近況報告

-* hogee
-* hogeee
+* 運転手 for 坂井さん
+* nkさんからGGJ のフィードバックが来ていたので wiki に反映
+* OSの講義VMが攻撃を受けて学科ネットワークに影響
+* いくつかの読み物
+
+
+# VM が攻撃を受けた話
+
+* kvm で起動していた受講生のVMが攻撃を受けた
+* vagrant で作成したイメージを kvm で起動しっぱなしだった
+* ネットワークはグローバルIPを使っていた
+* セキュリティが甘い状態で攻撃を受けてしまい、学科ネットワークに影響が出た
+* 現在は当該VMは shut off
+

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

-* fugaaa
-* fugafuga
+* 外部から攻撃されるので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)