講演資料

形式手法と脆弱性評定を
組み合わせたセキュリティ評価
アーク・システム・ソリューションズ株式会社
発表者：池田 和博
共著者：坂本 謙治
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
1
本事例の概要
• 情報セキュリティの評価・認証の基準を定めた国際規格
Common Criteria（ISO/IEC 15408）の脆弱性評定（AVA_VAN）を
用いたセキュリティ評価に、形式手法（本事例ではEvent-B）を
適用する。
実現できること
① 脆弱性評定の一部を事前に上流工程で実施
② 脆弱性の悪用可能性を形式手法で検証
Event-Bとは…
– 形式仕様記述と定理証明による検証が可能
– システムの環境も含めたシステム全体の検証が可能
 仕様の検証に適している
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
2
検証対象のシステム
• 本事例は経済産業省の支援事業を活用
– H24年度採択テーマ：『形式手法を活用した組込みセキュリティ技術の確立と、安心・安
全なCPS社会を支える無線通信ミドルウェアの開発』
• 検証に使用したシステムは宅内でのセキュアな無線通信ネットワークを
実現するための「無線通信ミドルウェア」を題材に実施した。
– 無線通信ミドルウェアは宅内で使用される機器に搭載され、認証・アクセスコントロー
ル機能を提供する。
 宅内に設置されるゲートウェイに対して、宅内機器の登録・認証を行い、
宅内ネットワークに参加する。
 不正な機器が宅内ネットワークに参加できないようにする。
MW
宅内セキュア
無線通信
MW
ゲートウェイ
MW
宅内ネットワーク
外部からの
無線接続による
脅威に対抗する
宅内機器
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
3
セキュリティ評価の課題
• 従来のセキュリティ評価の課題の一部
① 従来のレビューでは脆弱性検出の漏れ抜けが発生しやす
い。
– システムの複雑化や、ソフトウェア開発の規模が増大するなどが要
因となる。
② 上流工程ではシステム（仕様）の脆弱性に対する攻撃の検
証が困難である。
– 評価対象製品（Target of Evaluation：TOE）が開発前であるため、侵入
テストなどの実製品に対するテストは実施できない。
③ 上記から、セキュリティ評価はシステムや製品の開発完了
後に実施されるため、問題修正の手戻りが大きい。
– セキュリティ対策の不備を指摘された場合や、不具合の原因が設計
にある場合、大幅な手戻りによって工数が増大する。
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
4
上流工程の脆弱性評定と形式手法の適用範囲
• 開発者側が上流工程の設計成果物に対して事前に脆弱性評定を実施し
て、手戻りのコストを軽減する。
• 仕様書や設計書の不具合に起因する脆弱性を悪用する攻撃が可能か
どうか「形式手法（Event-B）」を利用して検証する。実装不具合に起因す
る脆弱性は「侵入テスト」で評価する必要がある。
評価の一般的なタイミング
従来手法（①～④）
と同様
手戻りの回避には、なるべく早い段階
で評価することが重要
形式手法の適用範囲
12th WOCS2
1/21/2015
CommonCriteriaの脆弱性評定フロー
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
5
機器の登録・認証シーケンス
•
•
無線通信ミドルウェアの「機器の登録・認証シーケンス」を検証の対象に選定した。
対象機能は、宅内機器（Dvc）が宅内ゲートウェイ（GW）に対して機器の登録・相
互認証を行い、アクセスコントロールを実現するものである。
【登録処理フェーズ】
Secret Key
Public key
Dvc
GW
Wi-Fi：Public key, Dvc ID
Public Keyのハッシュ値
とIDをディスプレイ表示
Dvc ID
PSK(*1)を生成
【ユーザー操作】
機器の登録開始
Wi-Fi：{PSK, Dvc ID}Public key of Dvc
PSKを保存
PSKとIDを保存
【認証処理フェーズ】
DTLS-PSKによるセキュアパスを設定、相互認証
【ユーザー操作】
機器の登録承認
or 登録拒否
*1：Pre-Shared Key
デバイスはホームネットワークに加入完了
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
6
脆弱性分析
• 無線通信ミドルウェアの仕様書や設計書を対象に「欠陥仮定法」を用い
て脆弱性の探索と仮定、および仕様書の分析を行った結果、機器の登
録処理において、存在する可能性のある脆弱性を識別した。
① 通信データの完全性：デバイス側の通信相手のなりすましの検証不備
② 通信の可用性：ゲートウェイ側のアクセス制御の不備
• 識別した脆弱性を対象に、Event-Bによる形式モデル化に必要な要素や
イベント（アクション）は、CRUD図を用いたデータのライフサイクルの観点
で分析・抽出した。
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
7
①通信データの完全性の検証
• 登録処理をEvent-Bモデル化した。
• 集合と定数、変数を定義した。
SETS
DVC, GW, KEY
CONSTANTS
Pub, Prv, Psk, Pair_Key
AXIOMS
partition(KEY, Pub, Prv, Psk)
Pair_Key ∈ Prv ⤖Pub …(A)
END
VARIABLES
request_msg, reply_msg, dvc_psk,
gw_reg_pub, gw_reg_id
INVARIANTS
request_msg ⊆ DVC × GW × Pub
reply_msg ⊆ GW × DVC × Psk × Pub
dvc_psk ∈ (DVC × GW) ↔ Psk
gw_reg_pub ∈ (GW × DVC) ↔ Pub
gw_reg_id ∈ (GW × DVC) ↔ Psk
dvc_key ∈ DVC ⇸ Pair_Key
∀dvc, prv, pub・
dvc ↦ (prv ↦ pub) ∈ dvc_key
⇒{dvc} ∈ dvc_key~[{prv ↦ pub}]
12th WOCS2
1/21/2015
A) 秘密鍵と公開鍵のペアは1対1の関係で
ある。
…(B)
…(C)
…(D)
…(E)
…(F)
…(G)
B) デバイスからゲートウェイに公開鍵を送
信。
C) ゲートウェイからデバイスにPSKを公開鍵
で暗号化して返信。
D) デバイスがゲートウェイから受信したPSK。
E) ゲートウェイがデバイスから受信した公
開鍵。
F) ゲートウェイがデバイスに対して生成した
PSK。
G) デバイスが生成した公開鍵と秘密鍵。
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
8
登録処理をEvent-Bモデル化
Req_evt …(1)
ANY dvc, gw, prv, pub WHEN
dvc ∈ DVC & gw ∈ GW &
prv ↦ pub ∈ Pair_Key &prv ↦ pub ∉ ran(dvc_key) &
dvc ∉ dom(dom(dvc_psk))
THEN
dvc_key := dvc_key ∪ {dvc ↦ (prv ↦ pub)}
request_msg := request_msg ∪ {dvc ↦ gw ↦ pub}
END
Req_rec_evt …(2)
ANY dvc, gw, pub, receiver WHEN
dvc ↦ gw ↦ pub ∈ request_msg &
receiver ∈ GW
THEN
gw_reg_pub :=
gw_reg_pub ∪ {(receiver ↦ dvc) ↦ pub}
END
• 機器の登録処理
1. デバイスは秘密鍵と公開鍵を生成
し、登録要求メッセージに公開鍵を
含んで送信。
2. 任意のゲートウェイ（receiver）が登
録要求メッセージを受信。
dvc_key
Prv
デバイスの
鍵生成
Pub
MW
request_msg
Dvc
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
MW
GW
9
登録処理をEvent-Bモデル化
Register_evt …(3)
ANY dvc, gw, pub, psk WHEN
gw ↦ dvc ↦ pub ∈ gw_reg_pub &
psk ∈ Psk & psk ∉ ran(gw_reg_id) &
gw ↦ dvc ∉ dom(gw_reg_id)
THEN
gw_reg_id := gw_reg_id ∪ {(gw ↦ dvc) ↦ psk}
END
Reply_evt …(4)
ANY dvc, gw, pub, psk WHEN
gw ↦ dvc ↦ psk ∈ gw_reg_id &
gw ↦ dvc ↦ pub ∈ gw_reg_pub
THEN
reply_msg := reply_msg ∪ {gw ↦ dvc ↦ psk ↦ pub}
END
Reply_rec_evt …(5)
ANY dvc, gw, pub, psk, receiver WHEN
gw ↦ dvc ↦ psk ↦ pub ∈ reply_msg &
receiver ∈ DVC
THEN
dvc_psk := dvc_psk ∪ {receiver ↦ gw ↦ psk}
END
12th WOCS2
1/21/2015
• 機器の登録処理
3. （ユーザーがゲートウェイのディスプ
レイをタッチして機器の登録を承認
した場合）ゲートウェイが事前共有
鍵を生成。
4. ゲートウェイが応答メッセージに事
前共有鍵を含んで、デバイスの公
開鍵で暗号化して送信。
5. 任意のデバイス（receiver）が応答
メッセージを受信。
reply_msg
MW
MW
Dvc
GW
Pskの生成と
暗号化
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
Psk
Pub
10
Event-Bモデルのリファインメント
INVARIANTS
∀dvc, gw, psk, pub・ …(6)
dvc ↦ gw ↦ psk ∈ dvc_psk &
dvc ∈ dom(dvc_key) & pub ∈ ran(dvc_key[{dvc}])
⇒ gw ↦ dvc ↦ psk ∈ gw_reg_id &
dvc ↦ gw ↦ pub ∈ request_msg
• ゲートウェイのなりすましの検証
Reply_rec_evt …(5)
REFINES
Reply_rec_evt
ANY dvc, gw, pub, psk, receiver, prv WHEN
gw ↦ dvc ↦ psk ↦ pub ∈ reply_msg &
receiver ∈ DVC &
prv ∈ Prv & Pair_Key(prv) = pub & …(7)
prv ∈ dom(ran(dvc_key)) &
receiver ↦ (prv ↦ pub) ∈ dvc_key
THEN
dvc_psk := dvc_psk ∪ {receiver ↦ gw ↦ psk}
END
• 機器の登録処理
上記(6)のINVARIANTがどのようなイベントが
実行された場合でも成立することを証明する
⇒証明できない場合、ゲートウェイのなりすまし
ができるということになる
12th WOCS2
1/21/2015
6. デバイスがPSKを受信したならば、その
PSKはゲートウェイが生成したPSKであり、
そのゲートウェイはデバイスが登録要求
メッセージを送信したゲートウェイである。
5. 任意のデバイスが応答メッセージを受信。
7. 応答メッセージの暗号化に使用された公
開鍵とペアとなる秘密鍵を任意のデバイ
ス（receiver）は持っている。
reply_msg
MW
MW
Dvc
GW
Pskの
復号化
Psk
Prv
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
Psk
Pub
11
攻撃者モデルの導入
Reply_evt …(4)
REFINES
Reply_evt
ANY dvc, gw, pub, psk WHEN
gw ↦ dvc ↦ psk ∈ gw_reg_id &
gw ↦ dvc ↦ pub ∈ gw_reg_pub &
dvc ↦ gw ∈ dom(request_msg) …(8)
THEN
reply_msg := reply_msg ∪ {gw ↦ dvc ↦ psk ↦ pub}
END
Spoof_Reply_evt …(9)
REFINES
Reply_evt
ANY atk, dvc, pub, psk WHEN
atk ↦ dvc ↦ psk ∈ gw_reg_id &
atk ↦ dvc ↦ pub ∈ gw_reg_pub &
atk ↦ dvc ↦ psk ↦ pub ∉ reply_msg &
dvc ↦ atk ∉ dom(request_msg)
WITH
gw = atk
THEN
reply_msg := reply_msg ∪ {atk ↦ dvc ↦ psk ↦ pub}
END
12th WOCS2
1/21/2015
• 機器の登録処理
4. ゲートウェイが応答メッセージに事前共
有鍵を含んで、デバイスの公開鍵で暗
号化して送信。
8. ゲートウェイは、デバイスが登録要求し
たゲートウェイである。
• 攻撃者モデル
9. 攻撃者が応答メッセージに事前共有鍵
を含んで、デバイスの公開鍵で暗号化し
て送信。攻撃者は、デバイスが登録要求
したゲートウェイではない。
MW
MW
Dvc
Fake Psk
Prv
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
Fake Psk
Attacker
12
攻撃者モデルの検証
•
「ProB」のModel Checkingによるモデル検査を利用して検証すると「反例」が検出
された。反例を分析した結果、なりすましを検証するために定義したINVARIANTに
違反しており、ゲートウェイのなりすましができることが判明した。
攻撃者が応答メッセージの
なりすましを実行した後、
デバイスが応答メッセージ
を受信したとき
INVARIANTが成立していな
いため、なりすましの攻撃
が成功したことになる
∀dvc, gw, psk, pub・
dvc ↦ gw ↦ psk ∈ dvc_psk &
dvc ∈ dom(dvc_key) &
pub ∈ ran(dvc_key[{dvc}])
⇒ gw ↦ dvc ↦ psk ∈ gw_reg_id &
dvc ↦ gw ↦ pub ∈ request_msg
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
(DVC1 ↦ GW2) ↦ KEY3
(DVC1 ↦ GW1) ↦ KEY2
13
再検証
•
登録要求メッセージの機密性を検証するため、「送信先と受信者が一致している
こと」を検証するINVARIANTを追加して検証すると「反例」が検出された。反例を分
析した結果、INVARIANTに違反しており、機密性が確保されていないことが判明し
た。
ゲートウェイが登録要求
メッセージを受信したとき
INVARIANTが成立していない
ため、デバイスが意図した送
信先と異なる相手が受信でき
たことになる
∀dvc,gw,pub･
gw ↦ dvc ↦ pub ∈ gw_reg_pub
⇒ dvc ↦ gw ↦ pub ∈ request_msg
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
(GW2 ↦ DVC1) ↦ KEY2
(DVC1 ↦ GW1) ↦ KEY2
14
通信データの完全性の検証結果
• デバイスがゲートウェイへ登録要求メッセージを送信する際、平文
で送信しているため第三者が盗聴できてしまう。
• その結果、第三者がゲートウェイになりすまして、デバイスの機器
登録を妨害できることがわかった。
• つまり、脆弱性を悪用した攻撃が可能であることが判明した。
【登録処理フェーズ】
Secret Key
Public key
Dvc
GW
Wi-Fi：Public key, Dvc ID
盗聴
PSK_Aを生成
Dvc ID
{PSK_A, DVC ID}public key
Public Keyのハッシュ
値とIDを表示
PSKを生成
PSK_Aを保存
Wi-Fi：{PSK, Dvc ID}public key
デバイスはPSK_Aを受信したため
認証処理フェーズへ移行している
12th WOCS2
1/21/2015
【ユーザー操作】
機器の登録承認
or 登録拒否
PSKとIDを保存
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
15
②通信の可用性の検証
INVARIANTS
∀gw・
gw ∈ GW & gw_resource(gw) > 0
…(1)
Req_evt …(2)
ANY dvc, gw, prv, pub WHEN
dvc ∈ DVC & gw ∈ GW &
prv ↦ pub ∈ Pair_Key & prv ↦ pub ∉ ran(dvc_key) &
dvc ∉ dom(dom(dvc_psk))
THEN
dvc_key := dvc_key ∪ {dvc ↦ (prv ↦ pub)}
request_msg := request_msg ∪ {dvc ↦ gw ↦ pub}
END
Req_rec_evt …(3)
ANY dvc, gw, pub, receiver WHEN
dvc ↦ gw ↦ pub ∈ request_msg &
receiver ∈ GW &
gw_resource(receiver) > 0
THEN
gw_reg_pub :=
gw_reg_pub ∪ {(receiver ↦ dvc) ↦ pub}
gw_resource(receiver) := gw_resource(receiver) - 1
END
12th WOCS2
1/21/2015
Reply_evt …(4)
ANY dvc, gw, pub, psk WHEN
gw ↦ dvc ↦ psk ∈ gw_reg_id &
gw ↦ dvc ↦ pub ∈ gw_reg_pub
THEN
reply_msg := reply_msg ∪ {gw ↦ dvc ↦ psk ↦ pub}
gw_resource(gw) := gw_resource(gw) + 1
END
• ゲートウェイのリソース消費の検証
1. ゲートウェイのリソース容量は0以上であ
る（リソースを消費しても枯渇しない）
• 機器の登録処理
2. デバイスは秘密鍵と公開鍵を生成し、登
録要求メッセージに公開鍵を含んで送信。
3. 任意のゲートウェイが登録要求メッセー
ジを受信。受信した際、リソースを1消費。
4. ゲートウェイが応答メッセージに事前共
有鍵を含んで、デバイスの公開鍵で暗
号化して送信。送信した際、リソースを1
解放。
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
16
攻撃者モデルの導入
VARIABLES
replay_request_msg
INVARIANTS
replay_request_msg ⊆ DVC × GW × Pub
replay_request_msg = request_msg …(5)
Wiretap_req_evt …(6)
= request_msg
ANY dvc, gw, pub, atk WHEN
dvc ↦ gw ↦ pub ∈ replay_request_msg &
atk ∈ DVC & atk ≠ dvc
THEN
atk_get_msg := atk_get_msg ∪ {atk ↦ gw ↦ pub}
END
Replay_attack_evt …(7)
REFINES
Req_evt
ANY atk, gw, pub WHEN
atk ↦ gw ↦ pub ∈ atk_get_msg
WITH
dvc = atk
THEN
replay_request_msg :=
replay_request_msg ∪ {atk ↦ gw ↦ pub}
END
12th WOCS2
1/21/2015
• 変数の再定義
5. 変数の置き換え：登録要求メッセージ(再
送含む)
• 攻撃者モデル
6. 攻撃者が登録要求メッセージを盗聴し、
デバイスの公開鍵を取得。
7. 攻撃者がデバイスの公開鍵を利用して、
ゲートウェイに登録要求メッセージを送
信（リプレイ攻撃）。
dvc_key
Prv
Pub
reply_ request_msg
(= request_msg)
MW
MW
Dvc
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
GW
Attacker
17
攻撃者モデルの検証
•
「ProB」のModel Checkingによるモデル検査を利用して検証すると「反例」が検出
された。反例を分析した結果、リソース消費を検証するために定義したINVARIANT
に違反しており、ゲートウェイのリソースが0になる（枯渇する）ことが判明した。
攻撃者が登録要求のリプレイ
攻撃を行い、ゲートウェイが受
信することを繰り返したとき
INVARIANTが成立していない
ため、ゲートウェイのリソース
が枯渇したことになる
∀gw·
gw ∈ GW & gw_resource(gw) > 0
12th WOCS2
1/21/2015
(GW1 ↦ 0)
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
18
通信の可用性の検証結果
• デバイスがゲートウェイへ登録要求メッセージを送信する際、平文で送信
しているため第三者が盗聴できてしまう。
• また、ゲートウェイは登録要求メッセージの受信を制限する機能がない。
• その結果、第三者が登録要求のリプレイ攻撃を利用したDoS攻撃を行い、
ゲートウェイのリソースを枯渇させることができるとわかった。
• つまり、脆弱性を悪用した攻撃が可能であることが判明した。
【登録処理フェーズ】
Secret Key
Public key
Dvc
Wi-Fi：Public key, Dvc ID
GW
盗聴
Public Keyのハッシュ
値とIDを表示
Dvc ID
Public key, Dvc ID
【ユーザー操作】
機器の登録承認
or 登録拒否
・
・
・
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
19
形式検証の結果のまとめ
• システム仕様をEvent-Bでモデル化し、攻撃者モデルを導入することで、脆弱
性を悪用した攻撃が可能かどうかを検証することができた。
検証内容
① 通信データの完全性 ⇒ ゲートウェイになりすました攻撃
② 通信の可用性 ⇒ リプレイ攻撃を利用したDoS攻撃
検証結果
1. 登録処理時の登録要求メッセージが漏えいする（2の根本的な原因）
2. 登録処理時の登録要求の応答メッセージがなりすまされる
3. 登録処理時の登録要求のDoS攻撃によりリソースが枯渇する
作業工数
•
•
•
Event-Bモデルの作成作業：4人日（システム仕様のモデル化、攻撃者モデルの導入）
Event-Bモデルの証明作業：1h程度（ほとんど自動証明、一部RodinのProverを利用）
Event-Bモデルによる検証：ほぼ無し（ProBのModel Checkingは一瞬で終了する）
項目
モ
デ
ル
規
模
①通信データの完全性の検証
②通信の可用性の検証
FirstModel
Refinement
AttackerModel
FirstModel
Refinement
AttackerModel
Step数
122
161
149
111
146
193
Event数
6
6
7
6
7
9
Variable数
6
6
6
6
9
10
Invariant数
7
6
1
7
3
4
証明課題数
14
21
8
16
17
24
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
20
考察
• 上流工程での脆弱性の検証
– 設計成果物から識別された脆弱性に対して、Event-Bを用いて検証を行った
結果、脆弱性を悪用した攻撃が可能であることが実証できた（⇒設計上の不
具合を検出した） 。
⟹製品テスト時に検出される設計要因の不具合を、上流工程で事前に検出す
ることで下流工程への不具合流出を低減させ、手戻りのコストを軽減すること
が期待できる。
• 形式手法の適用
– システムの処理やシーケンスを形式モデル化して、ProBのモデル検査に帰
着することで網羅的な検証を実現できることが実証できた。
⟹検証したい（保証したい）ことを一つのモデルに複数記述することで、網羅的
な検証により脆弱性検出の漏れ抜けを低減することが期待できる。
⟹形式手法による厳密な証明であり、検証の結果は客観的な判断基準として
利用することができる。
⟹実験の結果、形式モデル化に工数が掛かるとわかったため、システム全体を
モデル化するよりは、局所的（検証したい箇所）に適用することが効率的であ
ると考えられる。
12th WOCS2
1/21/2015
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
21
まとめ
• 検証する仕様や振舞いを「Event-B」によるモデル化と証明、さらに
「ProB」によってシステムの挙動を網羅的に検証することで、脆弱
性検出の漏れ抜けを低減することができる。
• Event-Bモデルに、攻撃者モデルを導入することで、脆弱性を悪用
した攻撃が可能か検証することができる。
• Common Criteriaの脆弱性評定を実施するためにEvent-Bを利用し
た検証を行い、設計に依存する脆弱性を上流工程で事前に検出
することで、下流工程で検出される設計上の不具合の指摘・修正
による手戻りのコストを軽減することができる。
12th WOCS2
1/21/2015
上流工程の欠陥に起因するもの
形式手法による検証
下流工程の欠陥に起因するもの
侵入テストによる評価
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
22
最後に
• 経済産業省－戦略的基盤技術高度化支援事業を活用
– H24～26年度採択テーマ「形式手法を活用した組込みセキュリティ技術の確
立と、安心・安全なCPS社会を支える無線通信ミドルウェアの開発」
経済産業省
産業技術総合研究所
名古屋大学
形式手法を活用した組込み
セキュリティ技術の確立と、
安全・安心な CPS 社会を支える
株式会社ヴィッツ 無線通信ミドルウェアの開発
Bメソッドで
実践開発を!!
委託
公立はこだて未来大学
川上・川下の連携による
コンソーシアム
アドバイザ
国内有数メーカ
川下企業
アーク・システム・ソリューションズ㈱
株式会社テクノフェイス
株式会社iD
12th WOCS2
1/21/2015
株式会社アトリエ
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
23
ご清聴ありがとうございました。
お問い合わせ先
アーク・システム・ソリューションズ株式会社
開発部 研究開発課 池田和博
TEL：011-207-6460
12th WOCS2
1/21/2015
e-mail：[email protected]
Copyright © 2015 Arc System Solutions Inc. All Rights Reserved.
24