Skip to content

Instantly share code, notes, and snippets.

@master-q

master-q/00memo.txt

Created November 16, 2017 10:31
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save master-q/3a64ca0cf0fdc274d516a1efd693f02d to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save master-q/3a64ca0cf0fdc274d516a1efd693f02d to your computer and use it in GitHub Desktop.
Download ZIP
seL4調査メモ
Raw
00memo.txt
= seL4
[2015-11-29 09:39]
<<< seL4
http://sel4.systems/
https://github.com/seL4
http://ssrg.nicta.com.au/projects/seL4/
https://wiki.sel4.systems/FrontPage
General Dynamicsって重工業系のコングロマリットらしい。つまり内部需要があるということ。
コントリビュートにはライセンス契約が必要。
http://sel4.systems/Community/Contributing/seL4-CLA.pdf
== 論文読んだまとめ
=== nicta_publication_full_7371.pdf
* 2.1. カーネル構成要素の説明: 権限,カーネルメモリ管理,仮想アドレス,スレッド,IPC,例外,デバドラ
* 2.2. カーネル設計プロセス:
* 証明による設計はトップダウン
* 要求とハードウェアに対する低レベルアルゴリズムからHaskellサブセットによるプロトタイプを作る
* このプロトタイプは自動的にIsabelle/HOLの動作可能な実装に落せる
* 最初の開発ステージではHaskellプロトタイプをQEMU上で実行させる
* Haskellプロトタイプを元にC言語実装を手動で設計
* このプロセスによって仕様とCコードが同期できる
* 最終的にHaskellプロトタイプは証明チェーンの一部にはならない (放置される？)
* 2.3. 形式的な検証:
* 最悪実行時間解析は実行バイナリの自動静的解析で
* Cとバイナリの変換は定理証明とSMTソルバで
* refinement: 抽象と具象を一致させること
* refinementによってホーア論理の性質は具象モデルでも保持される
* functional correctness: システムが正しく実装されているか
* capDL: システムの仕向け設定？
* Access Control + Information Flow: セキュリティの性質？
* abstract specification: システムの挙動に対する完全な仕様モデル。バイナリ中のシステムコールとか割り込みや仮想メモリ違反で何が起きるかとか。これがどのように実装されるかは含まない。
* executable specification: Haskellプロトタイプから定理証明器へ自動インポート。この仕様はCコードが持つであろう全てのデータ構造と実装を含む。
* IPC fastpath: fastpathの詳細な仕様であるexecutable specificationはあるが、抽象仕様はない。Cコードのfastpathがそのexecutable specificationを実装していることを証明したら、通常のIPCとfastpathが等価であるか証明する。
* C implementation: C言語のサブセット。証明器の中に書き写せる？
* 実行バイナリをHOL4に16進数ダンプし、その意味をCambridge ARM semanticsによって与える？
* 3. 検証のためのカーネルデザイン
* ホーア論理をベースにする
* 3.1. グローバル変数と副作用
* プリエンプションを限定し、Haskellからコードを生成することでグローバル変数の問題を扱いやすくしている
* seL4のトップにあるグローバル変数: 5つの配列、2つの整数、4つのポインタ
* Haskellプロトタイプを使うことでグローバル変数と副作用への依存を減らすことができた
* 3.2. カーネルの段階
* seL4のAPI呼び出しは2つの段階にわかれる: checking phaseとexecute phase
* checking phase: 引数を認証し、呼び出し権限を確認し、実行のための事前条件を確立する
* execute phase: 呼び出しを行ない、失敗しない
* 3.3. カーネルメモリ管理
* seL4では、権限の与えられたアプリケーションはカーネル内メモリ確保が行なえる
* アプリケーション毎にヒープを分割管理する
* メモリ確保は型なしメモリオブジェクトに型を割り当てることで行なわれる
* メモリ確保は型なしメモリオブジェクト中の有効メモリによって境界づけれられる
* カーネルオブジェクトは暗黙的に共有されたり、再利用されたりしない
* カーネル内アロケーションの正しさとは、1つの型なしメモリ領域に新たなオブジェクトが完全に含まれ、かつそのリージョンに確保された別のオブジェクトと重ならないか
* メモリブロックを再利用するにはそれへの全ての参照が無効化されなければならない
* 3.4. 並行性と非決定性
* 並行プログラムの証明は難しい
* 並行サポートは別の論文を見てほしい
* Yieldingはイベントベースのカーネル実行モデルで扱う
* Interruptに対して、seL4はほぼ割り込み禁止で動作する
* 4. FUNCTIONAL CORRECTNESS
* 4.1. Abstract Specification
== まずは使ってみる
http://sel4.systems/Info/GettingStarted/
リポジトリ構成:
* l4v the seL4 proofs
* seL4 the seL4 kernel
* verification, the seL4 proofs.
* seL4test, a test suite for seL4, including a Library OS layer.
* CAmkES, a component architecture for embedded systems based on seL4. See the CAmkES pages for more documentation about CAmkES.
* VMM a componentised virtual machine monitor for ia32 platforms using Intel VT-X and VT-D extensions.
* RefOS,, a reference example of how one might build a multi-server operating system on top of seL4. It was built as a student project.
以下のようなソース構成をビルドしてみた。当然このビルドプロセスではIsabelleの検証は走らない。
```
$ pwd
/home/kiwamu/src/seL4_repo
$ repo sync
$ ls -F
Kbuild@ Kconfig@ Makefile@ apps@ configs@ kernel/ libs/ projects/ tools/
$ make ia32_simulation_release_xml_defconfig
$ make
$ ls images
kernel-ia32-pc99* sel4test-driver-image-ia32-pc99*
$ make simulate-ia32
--snip--
136/136 tests passed.
All is well in the universe.
Ignoring call to sys_exit_group
Ignoring call to sys_rt_sigprocmask
Ignoring call to sys_gettid
Ignoring call to sys_getpid
sys_tgkill assuming self kill
```
上記を実行すると qemu-system-i386 -m 512 -nographic -kernel images/kernel-ia32-pc99 -initrd images/sel4test-driver-image-ia32-pc99 のようにqemuを使ってイメージが起動される。デフォルトでは各種テストコードが走るようだ。
テストケースは projects/sel4test/apps/sel4test-tests/src/tests にあるらしい。
ARM実機で動作させる手順: http://sel4.systems/Info/Hardware/General/
== テスコードの設計
https://github.com/seL4/sel4test を読む。
master-configsディレクトリはkernelのコンフィグファイル。
appsディレクトリにテストコードがC/C++で書かれている。
main関数は apps/sel4test-driver/src/main.c と apps/sel4test-tests/src/main.c の2箇所にある。
前者は後者を以下のようにして起動する。
```
error = sel4utils_spawn_process_v(&test_process, &env.vka, &env.vspace,
ARRAY_SIZE(argv), argv, 1);
```
== どうやって、何を検証しているのか？
検証の実行方法は以下:
http://sel4.systems/Info/GettingStarted/Proof
検証コードの構成は以下を参照:
https://github.com/seL4/l4v/#overview
```
$ pwd
/home/kiwamu/src/seL4_verify
$ repo init -u https://github.com/seL4/verification-manifest.git
$ repo sync
$ ls
HOL4/ graph-refine/ isabelle/ l4v/ seL4/
$ cd l4v
$ mkdir -p ~/.isabelle/etc
$ cp -i misc/etc/settings ~/.isabelle/etc/settings
$ ./isabelle/bin/isabelle components -a
$ sudo apt-get install openjfx openjdk-8-jdk
$ export ISABELLE_JDK_HOME=/usr/lib/jvm/java-8-openjdk-amd64/
$ ./isabelle/bin/isabelle jedit -bf
$ ./isabelle/bin/isabelle build -bv HOL-Word
```
物理メモリ8GBで検証してみる。
```
$ ./run_tests |& tee run_tests.log
Running 40 test(s)...
running isabelle ... pass ( 0:00:05, 0.62GB)
running CamkesAdlSpec ... pass ( 0:00:48, 3.52GB)
--snip--
```
file:///home/kiwamu/Dropbox/log/20160117_run_tests.log
テストドライバのPythonコードを調べれば、Isabelleの使い方がわかるのではないか？
l4v/misc/regression/run_tests.py のrun_test関数がテストドライバの大本。以下で実際の検証器を起動しているはず。
```
def run_test(test, verbose=False):
# Construct the base command.
command = ["bash", "-c", test.command]
--snip--
process = subprocess.Popen(command,
stdout=output, stderr=subprocess.STDOUT, stdin=subprocess.PIPE,
cwd=test.cwd)
```
つまりtest.cwdのパスでtest.commandを起動するということ。
通常run_testsは引数なしで起動されるので、testは以下のようにtests.xmlをカレントディレクトリから検索して順に実行する。
```
parser.add_argument("tests", metavar="TESTS",
help="tests to run (defaults to all tests)",
nargs="*")
args = parser.parse_args()
# Search for test files:
if not args.legacy:
test_xml = sorted(rglob(args.directory, "tests.xml"))
tests = testspec.parse_test_files(test_xml, strict=args.strict)
else:
--snip--
tests_to_run = []
if len(args.tests) == 0:
tests_to_run = tests
else:
--snip--
for t in tests_to_run:
--snip--
(passed, status, log, time_taken, mem) = run_test(t, verbose=args.verbose)
```
このテストのしくみは l4v/misc/regression/testspec.py で抽象化されている。
が、結局のところtests.xmlに書かれたmakeコマンドをtests.xmlが置かれたディレクトリで起動するだけのようだ。
CamkesAdlSpecを例にしてさらに調べてみる。とりあえずMakefile直たたきでテストを起動できた。
```
$ pwd
/home/kiwamu/src/seL4_verify/l4v
$ git grep CamkesAdlSpec | grep tests.xml
camkes/tests.xml: <test name="CamkesAdlSpec">make CamkesAdlSpec</test>
camkes/tests.xml: <test name="CamkesCdlRefine" depends="CamkesAdlSpec DSpec">make CamkesCdlRefine</test>
$ make -C camkes CamkesAdlSpec
make: ディレクトリ '/home/kiwamu/src/seL4_verify/l4v/camkes'　に入ります
/home/kiwamu/src/seL4_verify/l4v/isabelle/bin/isabelle build -b -v -d /home/kiwamu/src/seL4_verify/l4v"" CamkesAdlSpec
Started at 2016年 1月 19日 火曜日 18:19:07 JST (polyml-5.5.2_x86_64-linux on casper)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/kiwamu/.isabelle/contrib/polyml-5.5.2-3/x86_64-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 2000"
Session Pure/Pure
Session HOL/HOL (main)
Session CAmkES/CamkesAdlSpec (Camkes)
Finished at 2016年 1月 19日 火曜日 18:19:12 JST
0:00:05 elapsed time, 0:00:14 cpu time, factor 2.80
make: ディレクトリ '/home/kiwamu/src/seL4_verify/l4v/camkes' から出ます
```
この l4v/camkes/Makefile は以下のように変数を設定して、../misc/isa-common.mk をインクルードするだけ。
```
HEAPS += CamkesAdlSpec CamkesCdlRefine CamkesGlueSpec CamkesGlueProofs
GROUPS += Camkes
--snip--
include ../misc/isa-common.mk
```
../misc/isa-common.mk でisabelleコマンド起動をechoさせてみたところ以下を得た。
```
$ pwd
/home/kiwamu/src/seL4_verify/l4v
$ make -C camkes CamkesAdlSpec
make: ディレクトリ '/home/kiwamu/src/seL4_verify/l4v/camkes'　に入ります
/home/kiwamu/src/seL4_verify/l4v/isabelle/bin/isabelle build -b -v -d /home/kiwamu/src/seL4_verify/l4v CamkesAdlSpec
make: ディレクトリ '/home/kiwamu/src/seL4_verify/l4v/camkes' から出ます
```
あとはROOTファイルから先を理解できないといけないけど、これはIsabelleそのものに入門してからの方がいいかも。
```
$ pwd
/home/kiwamu/src/seL4_verify/l4v
$ find . -name tests.xml
./camkes/tests.xml
./spec/tests.xml
./sys-init/tests.xml
./tools/tests.xml
./proof/tests.xml
./misc/regression/tests.xml
$ find . -name ROOT
./camkes/ROOT
./spec/ROOT
./sys-init/ROOT
./tools/c-parser/Simpl/ROOT
./tools/c-parser/testfiles/ROOT
./tools/c-parser/ROOT
./tools/autocorres/tests/ROOT
./tools/autocorres/doc/quickstart/ROOT
./tools/autocorres/ROOT
./proof/ROOT
```
== binary-verification
ってのがあるらしい。Makefileターゲットに。
Raw
20160117_run_tests.log
Running 40 test(s)...
running isabelle ... pass ( 0:00:05, 0.62GB)
running CamkesAdlSpec ... pass ( 0:00:48, 3.52GB)
running CamkesGlueSpec ... pass ( 0:00:52, 3.06GB)
running tests-xml-correct ... pass ( 0:00:00, 0.00GB)
running SepTactics ... pass ( 0:01:13, 3.09GB)
running SepTacticsExamples ... pass ( 0:04:23, 3.98GB)
running ASpec ... pass ( 0:03:19, 4.47GB)
running ExecSpec ... pass ( 0:03:28, 5.07GB)
running AInvs ... pass ( 0:26:17, 5.38GB)
running BaseRefine ... pass ( 0:03:22, 5.27GB)
running Refine ... pass ( 0:42:44, 7.28GB)
running Access ... pass ( 0:10:27, 3.81GB)
running InfoFlow ... pass ( 0:19:30, 6.16GB)
running DSpec ... pass ( 0:02:29, 4.40GB)
running CamkesCdlRefine ... pass ( 0:34:39, 5.99GB)
running DBaseRefine ... pass ( 0:00:07, 0.83GB)
running DRefine ... pass ( 0:00:07, 0.91GB)
running DPolicy ... pass ( 0:00:06, 1.26GB)
running SepDSpec ... pass ( 0:02:31, 3.28GB)
running DSpecProofs ... pass ( 0:03:38, 3.36GB)
running TakeGrant ... pass ( 0:00:45, 3.08GB)
running ASepSpec ... pass ( 0:00:42, 2.62GB)
running Bisim ... pass ( 0:01:12, 3.80GB)
running SpecCheck ... pass ( 0:00:01, 0.01GB)
running SysInit ... pass ( 0:03:56, 3.35GB)
running SysInitExamples ... pass ( 0:04:01, 3.35GB)
running CParser ... pass ( 0:04:46, 3.60GB)
running CKernel ... pass ( 0:35:39, 7.06GB)
running CSpec ... pass ( 0:18:37, 5.02GB)
running CBaseRefine ... pass ( 1:44:08, 9.15GB)
running CRefine ... pass ( 6:23:40, 7.96GB)
running InfoFlowC ... pass ( 0:52:46, 7.24GB)
running SimplExportAndRefine ... pass ( 1:48:36, 5.06GB)
running CParserTest ... pass ( 0:19:19, 6.84GB)
running CParserTools ... pass ( 0:00:44, 2.35GB)
running AutoCorres ... pass ( 0:02:52, 3.34GB)
running CamkesGlueProofs ... pass ( 0:09:20, 5.28GB)
running AutoCorresDoc ... pass ( 0:00:22, 3.71GB)
running AutoCorresTest ... pass ( 0:20:49, 6.93GB)
running AutoCorresSEL4 ... FAILED * ( 2:00:59, 6.36GB)
------------------------------------------------------------------------
TEST FAILURE: AutoCorresSEL4
...
AutoCorresSEL4: theory SimplConv
AutoCorresSEL4: theory L2Peephole
AutoCorresSEL4: theory TypeStrengthen
AutoCorresSEL4: theory L2Opt
AutoCorresSEL4: theory WordAbstract
AutoCorresSEL4: theory Polish
AutoCorresSEL4: theory LocalVarExtract
AutoCorresSEL4: theory HeapLift
AutoCorresSEL4: theory AutoCorres
AutoCorresSEL4: theory TestSEL4
*** Timeout
AutoCorresSEL4 FAILED
(see also /home/kiwamu/.isabelle/heaps-home-kiwamu-src-seL4_verify-isabelle/polyml-5.5.2_x86_64-linux/log/AutoCorresSEL4)
Translating (type strengthen) performPageInvocationUnmap
--> nondet
Trace: "Converted (TS) performPageInvocationUnmap in 0.186 s"
Translating (type strengthen) invalidateTLBByASID
--> option
Trace: "Converted (TS) invalidateTLBByASID in 0.158 s"
Translating (type strengthen) pdeCheckIfMapped
--> option
Trace: "Converted (TS) pdeCheckIfMapped in 0.133 s"
Translating (type strengthen) performPageInvocationRemapPDE
--> nondet
Trace: "Converted (TS) performPageInvocationRemapPDE in 0.305 s"
Translating (type strengthen) pde_pde_section_get_size
--> pure
Trace: "Converted (TS) pde_pde_section_get_size in 0.164 s"
Translating (type strengthen) pde_get_pdeType
--> pure
Trace: "Converted (TS) pde_get_pdeType in 0.210 s"
Translating (type strengthen) pde_pde_section_new
*** Interrupt
Unfinished session(s): AutoCorresSEL4
Finished at 2016年 1月 17日 日曜日 16:32:43 JST
2:00:10 elapsed time, 3:08:07 cpu time, factor 1.56
Makefile:60: recipe for target 'AutoCorresSEL4' failed
make: *** [AutoCorresSEL4] Error 1
------------------------------------------------------------------------
39/40 tests succeeded.
Tests failed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment