--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2022/04/26.md	Wed Apr 27 00:10:04 2022 +0900
@@ -0,0 +1,66 @@
+# 研究目的
+
+## GearsOSにおけるメモリ管理とそれに対応する分散FS
+
+- アプリケーションの信頼性を保証するために，アプリケーションが動作するOSの信頼性を高める必要がある
+- 当研究室では，信頼性の保証を目的としたGearsOSを開発している
+- GearsOSで未実装の機能であるメモリ管理システムを構築、考察しそれに対応する分散FSを考察する
+
+(メモリと分散FSまとめて研究テーマにするとでかい気もするが、とりあえずそのまま。不可分な気もする。)
+
+要件
+
+- モデル検査による信頼性の保証
+  - CbCによるノーマルレベル、メタレベルの切り分け
+
+取り入れたい要素
+
+- transaction
+- backup & logging
+- unix like
+
+# 考え事や調べ物
+
+## スパースファイル
+
+スパースファイルとは部分的に空を含むファイルを実際のファイルシステム上では、空の代わりにメタデータと呼ばれる小さな情報を書き込むことにより効率的に保存する仕組みのこと。
+
+## Named Streams
+
+名前付きストリーム(Named Streams, Alternate Streams, Alternate Data Streams, ADS, 代替データストリーム)とは、デフォルトのファイルストリームに名前はついていないが、一つのファイルに複数ストリームを持たせようとしたときに、デフォルトのストリームと区別するために、名前をつける必要がある。そのストリームが名前付きストリームである。CTFのネタになる感じのものらしい。
+
+参考: https://infosecwriteups.com/alternate-data-streams-ads-54b144a831f1
+
+## journaling filesystem
+
+[Linux System Administrators Guide](https://tldp.org/LDP/sag/html/index.html)5.10.3 Which filesystem should be used?にて、
+
+> Currently, ext3 is the most popular filesystem, because it is a journaled filesystem. 
+
+という記述がある。今であればext4を選ぶだろう。この本は2000年ごろに原著が出たので、その頃の話ではあるが、journaled filesystemであることはファイルシステムを選ぶ上で重要な項目のようだ。確かに、NTFS、APFS、Ext4などの現在主に使われているファイルシステムはjournalingしている。よって、もはや当たり前の機能だと思われる。もし、journalingしていなければ、ファイルシステムの修復をする際にすべてのファイルについてメタデータと実データの整合性をチェックするので非常に時間がかかる。
+
+## Windowsのファイルシステム
+
+Windowsにはファイルシステムドライバーとミニフィルタードライバーというものがある。
+Windowsのファイルシステムはファイルシステムドライバーとして実装されるらしい。
+
+# GearsOS
+
+## お掃除
+
+- 必要なファイルだけ取り出す
+- また、LinuxカーネルのようにGearsカーネルという感じで、OSの主要機能をカーネル、付加機能をモジュールとして分けるような形にしたい
+- 不要なものをどうやって見極めようか
+- 読み会でもしながら掃除するといいかも
+
+「GearsOSお掃除読み会」
+
+## メモリ管理システム
+
+メモリ割り当ての想像
+
+- Gear単位でメモリに貼り付けるイメージ
+- Contextにページを割り当てる
+- Gearは割り当てられたページ内でallocateする
+
+他にも、free、fault handler、OMM Killer
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/mizuki/メモ/2022.md	Wed Apr 27 00:10:04 2022 +0900
@@ -0,0 +1,30 @@
+## 研究目的
+動作しているシステムに関する情報を収集することにより攻撃や故障の検出を行うことができる。  
+このとき膨大な情報の中から適切な情報を収集し、異常な情報を摘出し通報する必要ことが必要である。  
+この情報の選択を完全に自動で行うことができない、管理者とシステムが協調することによりこの問題を解決することを目的とする 
+
+## OS研究会
+近年のシステムの大規模化・複雑化もあり、ログの設定は多種多様で都度適切な設定をするのは難しい。  
+それらの設定を日々用いるメッセージングツールから行うことで管理者の負担が減ると考える
+
+### 案
+ほっといて動くはむずい  
+アップデートなどの警告についていく必要あり  
+ゼロデイ攻撃の対応、cephのファイル  
+情報の取捨選択を日々の作業のなかで作っていく 
+
+インタラクティブに設定する時にどんなAPiがあるか  
+ログの管理に対してどんな機能があるか  
+作業例があるとよい   
+このエラーメッセージに対してこの作業をしたという記録をとればいいな  
+
+こういうエラーログが重要なのでまとめていく  
+
+IPV4やめて６４変換だけにしたのでそれだけが外に出る  
+
+学内に接続するとV6あかつきが管理  
+外からみえるようにするしないの選択  
+暁でいちいちやるのではなくmmからやるように  
+
+日々のソフトのアップデートによってログメッセージも変化していき、また外部からの攻撃などにも対応する必要がある。
+その為、機械学習ではなく実際に発生したログと作業例を参考に使用できるログ設定の機能を調査し実装する
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/mizuki/メモ/2022/04/26.md	Wed Apr 27 00:10:04 2022 +0900
@@ -0,0 +1,30 @@
+## 研究目的
+動作しているシステムに関する情報を収集することにより攻撃や故障の検出を行うことができる。  
+このとき膨大な情報の中から適切な情報を収集し、異常な情報を摘出し通報する必要ことが必要である。  
+この情報の選択を完全に自動で行うことができない、管理者とシステムが協調することによりこの問題を解決することを目的とする 
+
+## OS研究会
+近年のシステムの大規模化・複雑化もあり、ログの設定は多種多様で都度適切な設定をするのは難しい。  
+それらの設定を日々用いるメッセージングツールから行うことで管理者の負担が減ると考える
+
+### 案
+ほっといて動くはむずい  
+アップデートなどの警告についていく必要あり  
+ゼロデイ攻撃の対応、cephのファイル  
+情報の取捨選択を日々の作業のなかで作っていく 
+
+インタラクティブに設定する時にどんなAPiがあるか  
+ログの管理に対してどんな機能があるか  
+作業例があるとよい   
+このエラーメッセージに対してこの作業をしたという記録をとればいいな  
+
+こういうエラーログが重要なのでまとめていく  
+
+IPV4やめて６４変換だけにしたのでそれだけが外に出る  
+
+学内に接続するとV6あかつきが管理  
+外からみえるようにするしないの選択  
+暁でいちいちやるのではなくmmからやるように  
+
+日々のソフトのアップデートによってログメッセージも変化していき、また外部からの攻撃などにも対応する必要がある。
+その為、機械学習ではなく実際に発生したログと作業例を参考に使用できるログ設定の機能を調査し実装する
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/soto/log/2022-04-26.md	Wed Apr 27 00:10:04 2022 +0900
@@ -0,0 +1,52 @@
+# 研究目的
+- 愚直にプログラムを書くと、冗長なコードができてしまい、実行時間も遅くなることがある。
+	- この場合に、コードに対してアルゴリズムを適応すると実行が最適化され実行時間が減り、かつ第三者がコードを読んだ場合にロジックが統一さてれいるため理解が容易くなる。一般的に言う良いコードが作成できる。
+- しかし、世の中にはアルゴリズムが大量にあり、これを一人のプログラマーが全て覚え、また適応できる場面を思いつくというのは不可能
+- そのため、人が愚直に書いたコードに対してアルゴリズムを使用するコードを自動で適用できるようにしたい
+
+- この場合、アルゴリズム適用前と適用後で同じコードになっていることを証明するのは難しい。
+	- 普通のプログラミング言語では恒等性を示す根拠が足りない
+
+- また、普通のプログラミング言語では、関数の遷移が自由であることにより、関数遷移などで発生した暗黙の環境(変数)が存在するため、アルゴリズムの適応を行うのは難しい
+
+- ここで、当研究室で開発している Gears Agda を用いる。
+    - Gears Agdaとは当研究室で開発している Continuetion based C (CbC)の概念を取り入れた記法
+	- 通常関数を遷移する際にはメインルーチンからサブルーチンに遷移する。この際メインルーチンで使用していた変数などの環境はスタックされる。しかしCbCの継続ではjmp命令で関数遷移を行い、スタックを持たず環境を保存しない。これにより暗黙な環境が存在せず検証がしやすくなる。
+
+- アルゴリズムの適用は現状以下の方法を考えている
+
+- Gears Agda にてあらかじめアルゴリズムの実装と検証を行ったアルゴリズムSetsを用意する
+
+- 事前に定義していたアルゴリズムのInvariantが書いたCodeGearに当てはめられるのかを調べていく
+    - 当てはまる場合にアルゴリズムを入れ替える
+
+## SIGOSに出す研究の目的
+- モデル検査といえば主流はSPIN
+- しかし、上述したアルゴリズム入れ替えの可否判定にはGears Agda 内部でモデル検査をするのが最も妥当であると考えている。
+    - バブルソートをマージソートに変える場合では定理証明を行っても内部動作が一致しないので、定理証明を行ったあとに使えない。
+    - (そもそも何も考えずに書いたコードを定理証明で証明するのはコストが高い)
+    - モデル検査でアルゴリズム側の不変条件(INvariant)を入れ替え元のCode Gearが満たしている場合に
+      入れ替える形になる。
+    - つまり、そのコード中で不変条件を満たしているのかをモデル検査で検証を行う
+- このことから、Gears Agda上でモデル検査を行う。
+
+- 課題として、Agda上では並列実行ができない。
+
+
+## 今週の進捗
+- 研究の申込みをした
+- mercurialにリポジトリを用意した
+- モデル検査について調べていた
+    - DPPをSPINで解いているものがあったので動かしたり遊んでみた
+
+- GearsAgda上のモデル検査
+    - DPP入力の網羅とかはいつかなかったのでassartの例題を作るなどしていた
+    - DPPの実装も並列の表現方法が思いついていない
+
+### assertについて
+- Meta Code Gearのように普通のMeta Code Gearの間に
+  はさもうと考えています。(現在はBoolが入っていますが…)
+- 欲を言えばassertにLTLが記述できるようになりたい
+- Meta Data GearはData Gearをwrapしてassert errorを格納できるとよいかと思っています。
+
+![meta_cg_dg.pdf](http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2022/soto-sigos/raw-file/tip/Paper/fig/meta_cg_dg.pdf)
\ No newline at end of file