■日時:平成29年9月15日(金) 11:30~12:30
■場所:国立情報学研究所20階 ミーティングルーム1(2010室)
東京都千代田区一ツ橋2-1-2
議題:
1)開会の辞
2)議長選出
3)議案
第1号議案 主たる事務所移転について
第2号議案 貸借対照表の公告について
第3号議案 理事の承認
2017年6月29日(木)に実施された「第19回 OSSユーザーのための勉強会」では、AI/Deep Learning 分野での活用が注目されているプログラム言語の「 Python 」を題材に、その概要から詳細な解説に至るまで、ご紹介していただきました。
今回の勉強会では、AI/Deep Learning 分野での活用が注目されているプログラム言語の「 Python 」をテーマに、その概要・特長・最新動向や、AI/Deep Learning 分野における活用について、株式会社ビープラウドの鈴木さん、株式会社CMSコミュニケーションズの寺田さんにご紹介していただきました。
また勉強会のあとの懇親会でも、参加者の有志の方から興味深く、熱いライトニング・トークが行われ、会場は参加者の熱気に溢れ、参加者同士の意見交換など活発な交流が行われました。
以下に発表資料を公開しております。
http://www.scsk.jp/product/oss/report2.html
・開催日時:2017年6月29日(木) 18:30~ (20:15終了予定、開場 18:00)
・プログラム
1.「 Pythonの特長と最新動向 」(仮題)
株式会社ビープラウド Python Climber、一般社団法人PyCon JP 理事 鈴木たかのり
2.「 AI/Deep Learning 分野におけるPythonの活用 」(仮題)
株式会社CMSコミュニケーションズ 代表取締役、一般社団法人PyCon JP 代表理事
寺田 学
3. Q&A、ディスカッション
~ 終了後 懇親会(参加無料)~
4. 参加者によるライトニング・トーク(LT):懇親会で実施
※ 予告なくプログラム内容が変更される場合がございます。最新の情報は以下
のページでご確認ください。
http://eventregist.com/e/ossx2017-06
※ 記載されている製品/サービス名称、社名、ロゴマークなどは該当する各社
の商標または登録商標です。
・問い合わせ、登録フォーム
以下のページからご登録ください。
http://eventregist.com/e/ossx2017-06
2017年2月23日(木)に実施された「第17回 OSSユーザーのための勉強会」では、データセンター自動化ツール(構成管理ツール)の「 Ansible とChef 」を題材に、その概要から詳細な解説に至るまで、ご紹介していただきました。
今回の勉強会では、データセンター自動化ツール(構成管理ツール)の「 Ansible とChef 」をテーマに、その特長・アーキテクチャ・最新動向・今後の展望について、日本IBMの高良さん、レッドハットの安斎さんにご紹介していただきました。
また勉強会のあとの懇親会でも、参加者の有志の方から興味深く、熱いライトニング・トークが行われ、会場は参加者の熱気に溢れ、参加者同士の意見交換など活発な交流が行われました。
以下に発表資料を公開しております。
http://www.scsk.jp/product/oss/report2.html
・開催日時:2017年2月23日(木) 18:30~ (20:15終了予定、開場 18:00)
・プログラム
1.「 Chef の概要と特長」(仮題)
日本IBM㈱ エキスパート・テクノロジー・アーキテクト 高良 真穂
2.「 Ansible の特長と最新動向 」(仮題)
レッドハット㈱ シニア・ソリューションアーキテクト 安斎 宗一郎
3. Q&A、ディスカッション
~ 終了後 懇親会(参加無料)~
4. 参加者によるライトニング・トーク(LT):懇親会で実施
※ 予告なくプログラム内容が変更される場合がございます。最新の情報は以下
のページでご確認ください。
http://eventregist.com/e/ossx2017-2
※ 記載されている製品/サービス名称、社名、ロゴマークなどは該当する各社
の商標または登録商標です。
・問い合わせ、登録フォーム
以下のページからご登録ください。
http://eventregist.com/e/ossx2017-2
1. Introduction to behaviour models
2. Modelling concurrency.
3. Brief intro to linear temporal logics
4. Controller synthesis in MTSA
5. Enactment of controllers
MTSA: http://mtsa.dc.uba.ar
本講義は英語にて行われます.
講師
Nicolas D’Ippolito助教, ブエノスアイレス大学
http://lafhis.dc.uba.ar/en/~dippolito
講師:坂本一憲(国立情報学研究所)
事前に指定口座に受講料をお振り込み下さい.請求書が必要な方は別途NPO法人トップエスイー教育センター事務局(inquiry@topse.or.jp)までお問い合わせ下さい.
2016年11月22日(火)に実施された「第16回 OSSユーザーのための勉強会」では、脆弱性スキャナーの「 Vuls 」を題材に、その概要から詳細な解説に至るまで、講演していただきました。
今回の勉強会では、脆弱性スキャナーの「 Vuls 」をテーマに、その概要から詳細な解説に至るまで、フューチャーアーキテクトの林さんと神戸さんにご紹介していただきました。
また勉強会のあとの懇親会でも、参加者の有志の方から興味深いライトニング・トークが行われ、会場は参加者の熱気に溢れ、参加者同士の意見交換など活発な交流が行われました。
以下に発表資料を公開しております。
http://www.scsk.jp/product/oss/report2.html
今回は脆弱性スキャンツール「 Vuls 」を題材に、その特長・アーキテクチャ・最新動向・今後の展望についてご紹介いたします。
また今回も、ユーザーからのご意見・ご要望を表明する場として、参加者によるライトニング・トーク(LT)の時間を設けています。
最新のOSS動向に触れるチャンスとして、お気軽にご参加ください。セッション終了後にはささやかな懇親の場を用意しております。
・開催日時:2016年11月22日(火) 18:30~ (20:15終了予定、開場 18:00)
・プログラム
1.「セキュリティの現状とOSSの応用」
フューチャーアーキテクト㈱ スペシャリスト 林 優二郎
2.「脆弱性スキャナーVuls徹底入門」
フューチャーアーキテクト㈱ スペシャリスト 神戸 康多
3. Q&A、ディスカッション
~ 終了後 懇親会(参加無料)~
4. 参加者によるライトニング・トーク(LT):懇親会で実施
※ 予告なくプログラム内容が変更される場合がございます。最新の情報は以下のページでご確認ください。
http://eventregist.com/e/ossx2016-11
※ 記載されている製品/サービス名称、社名、ロゴマークなどは該当する各社の商標または登録商標です。
・問い合わせ、登録フォーム
以下のページからご登録ください。
http://eventregist.com/e/ossx2016-11
CafeOBJは、代数的にシステムの仕様を記述し、その上の性質を証明することができる先端的な形式仕様言語の一つです。本講義では、CafeOBJを使った代数仕様言語の記述方法とシステムの性質を対話的に証明する方法を実際に支援ツールを使いながら学ぶことができます。
講義は2日間にわたって行われ、自然数やリストを使ったCafeOBJによる代数仕様記述の記述方法から、具体的な相互排他プロトコルを使った対話的な証明まで、ツールを通して体験していただけます。CafeOBJの開発者の一人である二木特任教授から直接学ぶことができるまたとない機会となっております。
当日会場に用意されたシンクライアントにて演習を行うことができます。ご自身のPCで動かしてみたいという方は、以下のページからCafeOBJ 1.5.5をインストールしてご持参ください。
※本講義は、2015年10月23日に行われた内容に「仕様計算(Specification Calculus)による場合分けの自動化」の解説と演習が追加されています。
講師:北陸先端科学技術大学院大学 ソフトウェア検証研究センター 特任教授 二木厚吉
以下のページから最新の講義資料をダウンロードできます。http://www.jaist.ac.jp/~kokichi/lecture/1609NII/
※講義資料は英語が中心となりますが、講義は日本語で行います。
「CafeOBJ入門」
(1) 形式手法とCafeOBJ: http://ci.nii.ac.jp/naid/110006664762
(2) 構文と意味: http://ci.nii.ac.jp/naid/110006664763
(3) 等式推論と項書換システム: http://ci.nii.ac.jp/naid/110006840405
(4) 証明譜による検証法: http://ci.nii.ac.jp/naid/110006990888
(5) 認証プロトコルの検証: http://ci.nii.ac.jp/naid/130004549136
(6) 通信プロトコルの検証: http://ci.nii.ac.jp/naid/10025982447
「セキュリティ検証の現場で使える形式手法のツールがあるのか?」という疑問を、制御/IoT機器のセキュリティ検証業務を実施していく上で感じるようになりました。同じような疑問を持ったエンジニアの方もいらっしゃると思います。
Microsoft社では、動的ソフトウェアモデル検査の考え方を用いて、OSやオフィスソフトの脆弱性診断を実施しています。ソフトウェアのコード中の条件分岐をできるだけ網羅するように、テストの入力データを試験の実行時に変化させる手法です。しかし、残念ながらその実装系(SAGE) は、一般には未公開でした。
この技術はもっと広範に使えるのではないか、と感じていたところ、最近では、オープンソースの実装系も登場し、アクティブに開発が進められています。今回のセミナーでは、この実装系を実際に動かすことで、現場までの距離感を掴んで頂ければと思います。対象をうまく絞れれば、または、Microsoft社のようにスケールさせれば、確かに使えるのかも、と実感できると思います。
こうしたツールが必要な背景には、IoT機器の増加に伴うセキュリティへの懸念、電力分野の制御システムおよびスマートメーターに関するセキュリティガイ ドラインの発行に代表される、制御システムのセキュリティへの懸念、があります。これらのセキュリティの検証も、機器の認証を取るだけであれば、ファジングツールによる過去の攻撃事例に基づくパケットと大量のパケットに対して仕様通りに機器が振る舞えれば十分です。しかし、ファジングツールに実装されていない独自プロトコルに対する攻撃やゼロデイ攻撃によるリスクを減らすためには、もう少し賢い検証ツールを使えることが間違い無く重要になります。
本セミナーでは、動的なバイナリ解析ツールであるTritonという実装系を用いて、セキュリティ検証に関して
・何ができるのか
・どうやっているのか
について、動作原理の解説と、例をハンズオン形式で実施することで習得できます。
当日はシンクライアントを使ってTritonの演習を行いますが、ご自身のPCで演習されたい方は、インストール手順(Triton-install-log.txt)を参考に、以下のサイトから最新のソースをダウンロードし、インストールしてくだしさい。
Triton: https://github.com/JonathanSalwan/Triton
本ツールは、以下の環境で動作を確認しています。
Ubuntu 16.04, libboost(1.55以上),libpython, libcapstone,
libz3(https://github.com/Z3Prover/z3.git), Pin
[前提知識]
デバッガの画面、抽象構文木(abstract syntax tree、AST)の表現をご覧になったことがあると面食らわずに理解しやすいと思います。また、Pythonの基礎知識があると、ハンズオンで利用するサンプルコードを理解する際に役立ちます。
[参考URL:]
SAGE: http://research.microsoft.com/en-us/um/people/pg/
Triton: https://github.com/JonathanSalwan/Triton
なお、その他の事例については、「ディペンダブル・システムのための形式手法の実践ポータル(http://formal.mri.co.jp/)」もご参照ください。
講師:松崎 和賢・(株)三菱総合研究所
13:00-14:00 セーフティーとセキュリティ概論 ~ 乗り物の安全の観点から ~
講師: 大久保 隆夫 氏(情報セキュリティ大学院大学・教授)
概要:近年、重要インフラへのサイバー攻撃が増加し、従来の機能安全とともに、セキュリティへの対策を講じることが必要になってきています。セキュリティを考える上で、従来の機能安全的手法でカバーできるのか、できないとすれば、どのようなアプローチが必要になるのか?セーフティとセキュリティ、前者は乗り物の製品開発において従来から考慮されてきた概念であり、後者はIT分野を中心に考慮されてきたものです。両者は,共通点もあるが相違もあるため、双方を実現するためには、手法も含め課題が多く存在します。本講演では、機能安全に代表されるセーフティとセキュリティの共通点と相違、それぞれの脅威、リスク分析の考え方について、乗り物を例に概説します。
14:00-15:20 組込みソフトウェアとセーフティ ~ 医療機器を題材に考える ~
講師: 宇佐美 雅紀 氏(国立情報学研究所 GRCEセンター トップエスイー 講師)
概要:モノのインターネット IoT(Internet of Things)は、大きな経済効果が期待できると言われていることもあり、大変な注目が集まっています。IoTのように、ソフトウェアが現実世界と密接に関わってくるようになると、今まで以上に安全性が重要になります。本講演では、安全性が最重要である医療機器のソフトウェアを題材にして、ソフトウェアにおける安全について考えます。安全なソフトウェアを作るための規格の要求、開発プロセスや技術に加えて、開発現場での苦労や工夫について説明します。本講演は、規格解説ではありません。様々な分野の方と一緒にソフトウェアと安全について考えてみたいと思います。
15:20-15:30 休憩
15:30-16:50 自動車向けセーフティ&セキュリティ分析の一考え方と事例紹介
講師: 稲垣 徳也氏 (株式会社デンソー電子基盤システム開発部セーフティ・
セキュリティ技術開発室)
概要:車業界では、自動運転社会におけるセキュアな車載製品開発の早期実現を目指し、ユーザへ安心・安全を提供するための開発スタイル確立の動きが活発化しています。現在、日・米・欧などで自動車向け開発プロセスの標準規格の検討が本格化していますが、車業界全体で足並みを揃えた規格化までにはまだ時間がかかります。本講演は、自動車向けのセキュリティ開発プロセス標準化の現状を解説し、車業界としてのこれまでの強みである「品質・安全」を活かしたセーフティ&セキュリティ分析の一考え方を事例とともに紹介します。
16:50-17:00 質疑