WikiLeaksの見方

わかりにくくないですか？ちょっとメモメモ

---

■１．アクセス

今だとIP直打ちがいいのかしら・・・

http://213.251.145.96/

にいくと、WikiLeaksの画面に行く。

最近話題の、アメリカの外交文書は、
Cablegate: 250,000 US Embassy Diplomatic Cables
をクリック
（説明とかあって、ちょっと下のほう。ま、上記リンクをクリックしてもらってもいいんだけど）

---

■見方

そうして出てきた画面＊を、すこしスクロール

左側。「Browse latest releases」に
公開された日があるので、適当な日をクリックすると、
記事の一覧が出る。

ま、一番上の記事のReference IDをクリックしてみると、
（秘密文書なので、画像は省略）
な感じで、秘密文書が出る。

「英語ジャン！」わかんねーよという人は、

livedoorの翻訳
http://translate.livedoor.com/

で翻訳させると、それとなくわかる（わかんねーか　＾＾；）

---

■そのほかに
上記＊の画面では、「Browse latest releases」（公開日）のほかに

Browse by creation date（作成日）
Browse by origin（作成元？）
Browse by tag（タグ）
Browse by classification（秘密のレベルに分けてある）

の見方がある。

12月3日(金)のつぶやき

09:23 from web
御茶ノ水付近の神田川の川の水位が、高い・・・
20:24 from web
忘れないようにメモメモ。ふつうのi*のツールがST-Toolで、セキュアトロポス用i*のツールがSecTro
by xmldtp on Twitter

i*を使って、情報セキュリティ国際評価基準(CC)のセキュリティ目標（ST)を作る方法

■まず、CCについて概略

評価対象：TOE
TOEが満たすべきセキュリティ目標（ST)＝部分的なセキュリティ要求仕様
→STの作成をどうするか？
　　　→STに書くべき内容と目次（パート１概説と一般モデルにある）
　　　→プロテクションプロファイル→ST作成時の参考、STのサブセット
　↓
　パート２：セキュリティ機能コンポーネント
　　　→セキュリティ機能カタログ集
　　　　　　→ST,PPはここから選択　　　
　↓
　パート３：セキュリティ保証コンポーネント
　　　→セキュリティ保証要件集：セキュリティの検査項目カタログ集
　　　　　　＋
　　　　評価保証レベル（EAL)

---

■STとセキュリティ要求仕様の対応

１．ST概要
　　　→システムの機能要求とハードウエア環境の概要

２．適合性主張

３．セキュリティ課題定義
　　　脅威→攻撃者アクター、攻撃タスク、ミスユースケース
　　　セキュリティ方針→ゴール・タスク
　　　前提条件→ゴール・タスク
　　　　　

４．セキュリティ対策方針→ゴールやタスク
　　　　TOEのセキュリティ対策方針
　　　　運用環境のセキュリティ対策方針
　　　　セキュリティ対策方針根拠
　　　　　→表で記述

５．拡張コンポーネント定義
　　　CCパート２、３以外
　　　　→ゴールやタスクで、CCパート２にないもの

６．セキュリティ要件
　　　セキュリティ機能要件
　　　　　CCパート２を使ったゴールやタスク
　　　セキュリティ保証要件
　　　　　範囲外
　　　セキュリティ要件根拠
　　　　　６．１と４．１を対応

７．TOE要約仕様
　　　　→SFR(セキュリティ機能要件）をあらわすゴールやタスクの詳細タスク　　　

---

■i*を使った場合

１．本来のI*モデルを作成する
　　　　　→黄色で書く

２．攻撃モデルを作成する
　　　　セキュアトロポスを使って
　　　　　→悪意を持ったアクター追加（赤で書く）

３．「３．セキュリティ課題定義」を作成
　　　脅威 : T.攻撃タスク

４．セキュリティ対策を含むドメインモデルを作成する
　　　　　→セキュリティのソフト作成
　　　　　→それに対する＋＋のゴール作成＊トップゴール
　　　　　→そのゴールに対する、CCパート２のゴールを作成
　　　　　　　　　→CCパート２のゴールになるまでゴール分解する
　　　　　→その結果、必要なものを追加

５．これらを踏まえて１章～２章
　　TOE概要
　　セキュリティ機能　４の＊トップゴール

６．４章を書く→３章は３で書いた
　４．１　セキュリティ対策方針
　　　　O.トップゴール

　４．３
　　　トップゴール　VS　攻撃タスク

７．６章を書く．セキュリティ要件
　　６．１　セキュリティ機能要件
　　　　→４で分解したCCパート２の内容を列挙
　　　　　CCの一部を書き換えて、使える
　　６．３
　　　　トップゴール　VS　６．１のCC

８．７章のTOE仕様を書く

テストと検証をまとめてみる

テストや検証について、その位置づけをまとめてみる。

---

■静的と動的

テストや検証には、

・プログラムを動かさないで解析する－１．静的チェック
・プログラム、ないしはシミュレーター等を「動かして」解析する－２．動的チェック

に主に分かれる

---

■１．静的チェック

　これは、大きくは、

・文法やお作法が合っているかどうか

　という、１－１レビュー的なものと、

・プログラムの仕様上、正しいものか

　という、１－２検証的なもの

に分かれる。

１－１は、文法規約のチェックとか、パーサー、コンパイラなど。

１－２検証的なものは、形式仕様記述を利用したものが、さまざまある。たとえば
　　Z
　　Event-B、B
　など。どちらも、証明していく形でチェックする。
　Zは、仕様の断片とか、規約レベルでもそれぞれの規約をスキーマとして定義して、検証できる。
　Event-Bのほうが、もちょっとプログラム的かな？
　ただ、どちらも、似たようなことが出来る。Bは、Event-Bより、詳細といえる。

　Zも、Event-Bも、やる気になれば、データを入れた、動的チェックに近いことも出来る。
　一方、VDMは、基本的に動的チェックだが、最近、証明させる形の静的チェックもできるようだ。
　OCLは、びみょー。クラスを陰仕様のような形で書けるが、それで、どーなのよといわれると・・

---

■２．動的チェック

　動的チェックは、

　２－１．プログラムを実際動かし、確認する

　２－２．シミュレーションを行い、総当り的にチェックする

　の２種類。



２－１．プログラムを動かすものが、普通のテストに相当する。
　また、形式仕様のVDMは、テストデータを作って、設計仕様レベルのチェックができる。
　(一般のテストは設計ではなく、実装したもののテスト）
　データのテストとしては、OCLがあり、
　Javaの実装したものを、DbCに基づき、事前事後条件を形式的に記述、確認するものとしては、JMLがある。


２－２．のシュミレーションを使った総当りチェックは、モデル検査の分野である。

　モデル検査としては、並行時の動きを、設計レベルで調べるSPIN,SMV、LTSA、
　さらに時間概念を加えたuppaalなどがある。
　Javaを利用したものとしては、JPFがある。

　また、並行時の動きの詳細化を調べるものとしては、FDRがある（CSPで記述）
　これをJavaレベルでしらべる、JCSPってのもある。

---

ざっくり言うと、こんな感じかな・・・

astah*を使って、ICONIX風一気通貫システム開発 その５：属性を埋める

「astah*を使って、開発の要求仕様から、プログラム作成までを、トレーサビリティを保って、どのように開発するかを書いてみる」という、このシリーズ、以下の手順で説明する予定ですが、

（１）作るべきもののユースケースを書く
（２）ユースケースシナリオを書く
（３）ロバストネス分析
（４）バウンダリ（画面）、エンティティ（テーブル等）の属性を埋めていく
（５）バウンダリの項目を元に、画面構成を考える。
（６）(必要があれば）エンティティを正規化して、ER図にする
（７）フレームワークを決定する
（８）画面クラスをソースコードに書き直す
（９）エンティティをDBのテーブルと、DAOに書き直す
（１０）コントローラーを書き直す

前回、（３）をやったので、今回は、「（４）バウンダリ（画面）、エンティティ（テーブル等）の属性を埋めていく」について。

---

■ロバストネス分割が終わった後

　ロバストネス分析が終わると、画面とエンティティの名前はきまる。
　でも、
　　　・まず、その中の属性は、わからない

　　　・１ユースケース１画面になっているので、画面単位としては大きすぎる
　　　　　　　ユースケース：「受注を修正する」だと、「受注修正画面」になってしまうが、
　　　　　　　　　一般には、修正は、一覧を出して、そこから修正レコードをクリックしてもらい、
　　　　　　　　　その後、詳細(編集）画面を出して、そこから修正してもらう。
　　　　　　　　　つまり、「受注一覧」と「受注詳細」の２画面になる。

　　　・エンティティは正規化されているわけではないので、一貫性を持って
　　　　保存しなければならないデータが、分散されている可能性がある。

　そこで、これらの問題を解決し、画面構成とエンティティ構成（DBのテーブル構成）を決めていくのが、ここでの課題である。

---

■アプローチ方法

　画面構成とエンティティ構成（DBのテーブル構成）を決めるために、以下の作業を行う。

（あ）バウンダリの出力項目(属性）をとりあえず決める

（い）判っているところ（属性）をとりあえず埋める

（う）ユースケースシナリオあるいはアクティビティ図にしたがって、操作したとして、
　　　（あ）で決めた出力が得られるかどうか確認する
　　→得られない場合、（い）に項目追加などして、もういちど（う）、
　　　得られるまで、（い）と（う）を繰り返す

（え）指針を決めて、画面を分ける

（お）指針を決めて、エンティティ部分を決める

このとき、（え）は、全体では「（５）バウンダリの項目を元に、画面構成を考える。」にあたり、（お）は、全体では「（６）(必要があれば）エンティティを正規化して、ER図にする」にあたります。

　ということは、（４）は、（あ）、（い）、（う）をやればいいわけです。

---

■具体的方法：（あ）バウンダリの出力項目(属性）をとりあえず決める

　出力するもの＝成果物のクラス（バウンダリ）は、「（３）ロバストネス分析」で埋まっているはずです。

　埋まってなかったら、バウンダリに追加してください。
　　　それは、どこかのコントロールに所属するはずです。
　　　どこに所属するかというと、ユースケースシナリオに書いてあるはずです。
　　　　　　線で結んでください

　　　　　　書いてなかったら、ユースケースシナリオが間違っていますから、
　　　　　　　　どこで、出力すべきか考え、
　　　　　　　　ユースケースシナリオを書き直して、
　　　　　　　　「（２）ユースケースシナリオを書く」の手順に戻ってください

　いいですか、出力するもののバウンダリ、クラスはできてますよね。
　そこに、出力項目を、属性として、がんがん追加してください。
　出力すべき項目、たとえば、受注票、納品書の項目は、帳票レイアウトなり、
　実物の帳票を見れば判るはず。

　　もし、考えてなければ、今、考えてください。
　　帳票だけでなく、画面の出力項目も同様です。

　　ただし、考える際、項目だけで、レイアウトはまだいいです。

---

■具体的方法：（い）判っているところ（属性）をとりあえず埋める

　出力を受けて、入力項目を考えるのですが、
　とにかく、とりあえず、画面や帳票、エンティティで判ってるところは、
属性(項目）を、全部埋めちゃってください。

　エンティティに関しては、ドメイン分析をしていれば、その内容を埋めていけばいいし、
　その他でも、とにかくとりあえず、埋めてください。
　もちろん、このとき、完全じゃなくっていいです。適当なところで・・・

　完全性は、（う）で担保します。

---

■具体的方法（う）：出力が得られるかどうか、確認する

　そうしたら、ユースケースシナリオ等にもとづいて、入力から、出力までの操作を追っていきます
　(逆に、出力から入力を追って行っても良い）。

　出力するデータ項目を入力データ項目(画面等のバウンダリの属性＋エンティティの属性）から得られない／作れない場合は、入力項目が足りませんので、その足りない項目を追加します。
　追加する際、どこのバウンダリに項目追加すればいいかを考えて、追加します。

　追加＝（い）の行為に相当しますので、（う）をやり直します。

---

ちなみに、（う）の行為が検証ということになります。
この検証を、ソースコードレベルでやってしまうと、アジャイルになり、
形式仕様言語で記述して行うと、検証っぽくなります。
もっとも、アジャイルの場合は、（う）、（え）、（お）を一貫して行いますが・・・

ということで、（４）はおしまい。

12月2日(木)のつぶやき

18:21 from web
”ついに宇宙人発見か？　NASAが「宇宙生物学的発見」の会見へ”だそうな 　http://headlines.yahoo.co.jp/hl?a=20101202-00000016-cnn-int
by xmldtp on Twitter

Z その３ 証明とテスト

わすれそうなので、ちょっとメモ

---

■証明方法

theorem なんとか
　条件

という形で、証明したいことを書く。

まず、編集して、command→check all paragraphを行うと、
proof（左から２番目）がNになるときがある

このとき、証明できていないので、自分で証明する必要がある。
Nのところを選択して、右クリックすると、

　　　Show　Proof

というのがでてくる。それを選択すると、新しいダイアログが開く。
下に、式が書いてある。

　　全部選択して、
　　Reductionボタンをクリック、
　　prove by reduceをやってみる

うまくできたら、それでよし

うまくいかなかったら、自分で証明する必要があるので、適当に選んで
　　Reductionボタンをクリック、
あぷらいなんとかとか、simplifyとかあるので、てきとーに選ぶ

---

■theorem以外で、ProofがNになる。

　theoremをかかなくても、条件上、証明しないといけないときに起こる。
　この証明は、windowボタンのtheoremsを見ればわかる。
　そこから見たいものをダブルクリック。右側に証明がでる。

　ちなみに、これを直したいなら、specification画面に戻って、
普通の証明のように、右クリック、show proofを出す。
　あとは、証明できる。

---

■テスト

　この証明を使って、テストすることができる。
　スキーマ名[変数名 := 値]
　の形で書くと、値が設定できる。

　そこで、こうなっていてほしいという（要するに事後条件）を
　theoremで書けば、証明のチェック（演繹）で、値の変化や、正しいかどうかがわかる。

RFPの目標とかを受けて、提案書になって、その提案書が要求仕様書にはいるよねえ？

　あれ、ちょっと気になったので・・・
　RFPと提案書と要求仕様書の関係。

　RFPで、ふつう、
　　・提案してもらいたいシステムの概要（範囲とか、背景とか）
　　・目的・目標ないしはゴール（課題の場合もある）
　を書くよねえ（ここもそうだし、ITコーディネーター協会のRFP/SLA見本もそう）

　で、その目標や目的、課題などを受けて、提案書が作られる。

　さすがに要求仕様書は、提案書とは無関係に書けず、
　目的・目標、課題にかんするソリューションは、
　要求仕様書にはいってきて、

　その際、IEEE830だと、１章の「はじめに」の目的、範囲が、RFPの目的やその他もろもろに合致しているはずってことになるんだよねえ・・・

　対応関係で言うと・・・

VDMのお勉強－その７ VDMを書こう！ VDM++版概略

シリーズ「VDMのお勉強」。

前回は、VDM－SLで、「名前を入力したら、
　”Hello ”＋名前＋”!!"
と出力する処理、Helloを定義」した。
今回は、ついでに、まったく同じコトを、VDM++で定義してみたいと思う。

---

■overtureの出力

　overtureで、VDM++のクラスを生成すると、自動的に以下のように書かれる。

class HelloVDM
	types
-- TODO Define types here
	values
-- TODO Define values here
	instance variables
-- TODO Define instance variables here
	operations
-- TODO Define operations here
	functions
-- TODO Define functiones here
	traces
-- TODO Define Combinatorial Test Traces here
end HelloVDM

---

■サンプルコード

これに、上記のメソッドを書くんだけど、昨日のVDM-SLと同じように直す。
そうすると、こんなかんじ

class HelloVDM
types
--	ここに、型とか書くけど、今回は使わない

values
--	ここに、定数とか書くけど、今回は使わない

instance variables
--	ここに、インスタンス変数とか書く
-- public(private) 変数名 : 型 := 初期値; の形で書くけど、今回は使わない

-- 	不変条件
--     inv 条件式の形で書くけど、今回は使わない

functions
-- 関数を書くんだけど、今回は使わない

operations
public Hello : seq of char ==> seq of char
Hello(名前) ==
(
	return "Hello " ^ 名前 ^ "!!"
)

-- 事前条件：
pre len 名前 > 0;

-- 事後条件：
-- post 条件式だが、今回は特にない

traces
-- これを使って、あーしてこーしてテストすると、
-- かっこよく出来るんだけど、そもそも、今回テストしない

end HelloVDM

---

■そして

　このソースを、VDM++用のVDM toolで開く。
VDM++用なんだけど、使い方は、
VDMのお勉強－その４　使い方
http://blog.goo.ne.jp/xmldtp/e/e08a21fa14c65253fa145563935571bb
で書いたVDM-SL用ツールと同じ。

まず、プロジェクト→ファイルの追加で読み込み、
　　　車両通行止めみたいなアイコンをクリックすると、実行ウィンドウが出てくる。

そこで、

init
create h := new HelloVDM()
debug h.Hello("vdm")

と入力すると、上の実行ウィンドウに

"Hello vdm!!"

と表示される。

12月1日(水)のつぶやき

09:38 from web
国交省のアンケート、大都市交通センサスかいてるんだけど、利用路線、「地下鉄」の書き方が判らない！JRは、東日本旅客鉄道と書くらしいけど、そうすると、地下鉄は（営団でなく）東京地下鉄？でも、東京地下鉄丸ノ内線だと、欄に入らない…
09:44 from web
まじ！iPadでastah*が動くの？ RT @hiranabe : astah* の iPad版、ET2010にて展示（ET2010 東洋テクニカさんのブース）。全くの新規開発で、手軽にほいほいクラス図描けます。触ってみてください。
by xmldtp on Twitter

VDMのお勉強－その６ VDMを書こう！ VDM-SL版概略

超久々に、シリーズ「VDMのお勉強」。

前回は、overtureを使って、VDM－SLの骨格を出力させた。
こんな感じ

module HelloVDM
exports all
definitions 

	state StateName of
 
-- TODO Define state here
	end 

	types 
-- TODO Define types here
	values 
-- TODO Define values here
	functions 
-- TODO Define functions here
	operations 
-- TODO Define operations here
end HelloVDM

今回は、書く中身について、概略。

---

■とにかく、サンプルコード
名前を入力したら、
　”Hello ”＋名前＋”!!"
と出力する処理、Helloを定義すると、こんなかんじ

module HelloVDM
exports all
definitions 

types 
--	ここに、レコードの型とか書くけど、今回は使わない

values 
state StateName of
-- 	ここに、状態として、
-- state HelloVDM管理 of 
-- 	変数 : 型という形で書いていくけど、今回は使わない

-- 	不変条件
--		inv mk_HelloModule管理(変数１,変数２・・・) == 
-- 		以降、不変条件を並べるけど、今回は使わない
--	初期化
--		init HelloVDMデータ == HelloVDMデータ
--                   = mk_HelloVDM管理(変数１の初期値,変数２の初期値・・・)
--	という形で書いていくけど、今回は使わないので書かない
end 


functions 
-- 関数を書くところ。今回は使わない。

operations
Hello : seq of char ==> seq of char
Hello(名前) ==
(
	return "Hello " ^ 名前 ^ "!!"
)

-- 事前条件：
pre len 名前 > 0;

-- 事後条件：
-- post 条件式だが、今回は特にない


end HelloVDM

---

■そして

　このソースを、
VDMのお勉強－その４　使い方
http://blog.goo.ne.jp/xmldtp/e/e08a21fa14c65253fa145563935571bb
で書いたツールを立ち上げて、ファイルを追加し、
実行用のパネルをひらいて、

init
print Hello("vdm")

と入力すると、

"Hello vdm!!"

と返ってくる。

---

細かい話の前に、同じコトをVDM++でもやってみる。

DIとアスペクト指向の共通点と相違点

　DIとアスペクト指向は、似ているところもある。

　どちらも、後から実体を注入することが出来る点だ。
　DIは、「依存性の注入」なので、出来るのはもちろんだけど、
　アスペクト指向でも、aroundとかを使うと、後からプログラムの実体を入れることが出来る。

---

　しかし、決定的な違いがある。

　DIは、実体を後から入れるが、構造は、前もってinterfaceで定義し、実体とインターフェースの関係を、設定ファイル（Springだとbean-conf.xml,Seasar2の場合diconファイル）で記述してしまう点だ。したがって、注入するクラスは、このインターフェースの構造に従う＝束縛される。

　一方、アスペクト指向は、インタータイプ宣言などにより、利用するメソッドや属性を追加させ、構造を変えてしまうことも出来る＝束縛されない。

---

　このような「アスペクト指向の何でも出来てしまう自由」は、（自己責任という名において）危険性と紙一重の関係にあり、あまりにひどい変更を行ってしまうと、コンパイルエラーになることすらありえる。

　したがって、フレームワークの「ハリウッドの法則」のような、拘束をかけたい場合は、自由なアスペクト指向ではない、DIのほうが向いている。

---

　ここで、昨日の状態遷移との問題がある。

　アスペクト指向では、遷移すら変えてしまう。優先順位を間違えれば、遷移の順序も変えてしまうし、ポイントカットをミスれば、不必要なときに呼び出しをしてしまったりする。
　このことは、派生開発などにアスペクト指向を使うことに対して、障害となる。

　アスペクト指向を利用すれば、構造も振る舞いも変えられる。
　そこで、これを利用して、既存のシステムに機能追加をすることが考えられる。
　しかしこの場合、設計上で想定しなかった遷移が起こる可能性がある。
　この点をどうするかを考えないといけない。