ESSoS 2012

情報セキュリティ研究室 > 学会/セミナー報告 > ESSoS2012
###  参加報告:International Symposium on Engineering    ###
###   Secure Software and Systems (ESSoS) 2012         ###

【会議名】International Symposium on Engineering Secure Software and Systems
          (ESSoS) 2012
【開催日】2012年2月16日(木)〜2月17日(金)
【場  所】Eindhoven University of Technology, Netherlands
【 URL  】http://distrinet.cs.kuleuven.be/events/essos/2012/index.html
【主  催】ACM SIGSAC, SIGSOFT, IEEE CS
【参加者】約40名
【予稿集】Springer  LNCS 7159
【報告者】松本研究員


+++++++++++++++++++++++++++++++++++++++
所感
+++++++++++++++++++++++++++++++++++++++
参加者は40名ほど、8割は欧州各国からで、残りは米国、アジアから数名の参加、日本からは報告者一名であった。
セッションは単一スレッドであり、全ての発表を聴講できた。
発表のテーマは、コンピュータシステムの開発および検証に関するものと、既存システムの理論的な脆弱性の分析に関するもので構成されていた。

発表の形態として、全体の半分はIdea Paperと呼ばれる、構想段階のものをまとめた未実装/検証の研究についてのだったが、非常に壮大なものを感じさせる発表もあった。最終セッションの"Typed Assembler for a Crypto-Processor"は、暗号文をそのまま処理するプロセッサについての発表であり、フィージビリティについては(現時点では詳細は述べられないとのことわりがあり、不明な点も多かったため)即断しかねるが、興味深かった。

基調講演は2件、各開催日の冒頭のセッションで行われた。
初日の基調講演"Improving Software Reliability and Security via Symbolic Execution"は、形式手法をセキュリティ要件検証に適用するものだが、同じ機能を持つ複数の実装をクロスチェックすることでセキュリティ上の問題点を検証するという考え方は(適用対象は限られるが)、有効だと感じた。
二日目の基調講演"An Overview of Modern Security Threats"では、現代のコンピュータシステムのセキュリティ上の脅威についての概観だったが、攻撃側のモチベーション源である経済的側面に着目しようという意見が印象深かった。


+++++++++++++++++++++++++++++++++++++++
所感
+++++++++++++++++++++++++++++++++++++++
■基調講演1: Improving Software Reliability and Security via Symbolic Execution
  Cristian Cadar(Imperial College)
・Dynamic Symbolic executionへの注目
・三つのツール EGT, EXE, KLEEを開発
    Cコードを基に制約セットを抽出, STPにかける
・スケーラビリティ上の問題に対して、Path探索、Pathの削除が重要
   ‥Coverage-optimized search, Best-first search, Random path searchなど
   ‥冗長なパスの削除  かなり劇的だが、カバレッジが早期に飽和する。カバレッジの
     満足は難しい
   ‥静的なパスのマージ  Phi-node foldingによるパス削減
   ‥Irrelevant Constraint EliminationとCachingの組み合せで劇的な高速化
・Semantic Bugsの検査について、Assetionを書く方法に対して、クロスチェッキングを行う方法がある。
   ‥クロスチェッキングを行うことで、仕様を記述する必要が無くなる
   ‥クロスチェッキングの例: OpenCVのリファレンス実装と、SIMD最適化コード
     をクロスチェックする
     …発見したバグの例:最小値を求める min(a, b)が、リファレンスでは一方がNaN
        の時は成立しないのに、値を返す場合がある。
    ‥別の例1:GNU coreutilとbusyboxでクロスチェック
    ‥別の例2:ZeroConfプロトコル実装、AvahiとBonjourでクロスチェック


セッション:Formal methods
座長: Cristian Cadar(Imperial College)
■Runtime Enforcement of Information Flow Security in Tree Manipulating Processes
  Mate Kovacs and Helmut Seidl(Technical Universtat Munchen, Germany)
・XML操作ソフトウェアにおいて情報フローポリシイを課す際の問題に、一般化されたconstant propagationを応用
  ‥オリジナルのConstant Propagationはあまりにも不正確
・文書投稿システムの例
   ‥XML文書の構成と、データ構造の対応

■Formalisation and Implementation of a Standard Access Control Mechanism for Web Services
 Massimiliano Masi(Tiani "Spirit" GmbH, Universita degli Studi di Firenze),
 Rosario Pugliese(Universita degli Studi di Firenze) and Francesco Tiezzi
 (IMT Advanced Studies Lucca)
・Polcy Based Access Control(PBAC)について、XACML: eXtensible Access
  Control Markup Languageがある。しかしXMLベースであるため、以下の問題が
  ある。
  ‥一般的なエディタでは記述困難
  ‥XACMLポリシイの記述は難しく、エラーを防ぎにくい
 ・XACMLはフォーマルなセマンティクスを持たないことから、形式化を行う
   XACMLの実装
   Java(パーサはANTLR)で実装
    BNF類似構文で描かれたポリシイをJavaクラスに変換する。

■Hunting Application-Level Logical Errors(Idea Paper)
 George Stergiopoulos, Bill Tsoumas and Dimitris Gritzalis(Information
 Security and Critical Infrastructure Protection Research Laboratory Dept.
 of Informatics, Athens University of Economics and Business(AUEB))
・App LogGICと呼ぶ、LV(Logical Vulnerability)解析のためのフレームワークの提唱。以下の2要素からなる
  ‥IBM(Invariant-Based Analysis Method)
    動的解析と静的解析のコンビネーション、
  ‥IEM(Information Extraction Method)
    ASTを解析し、IBMの出力のフィルタに必要な情報を抽出

セッション: Mobile devices
座長:Wouter Joosen(KU Leuven-DistiNet research Group)
■Challenges in Implementing End-to-End Secure Protocol for Java ME-Based Mobile Data Collection in Low-Budget Settings(Idea Paper)
 Samson Gejibo, Federico Mancini, Khalid Mughal, Jorn Klungsoyr and Remi
 Andre Valvik(Department of Informatics University of Bergen, Norway)
・Mobile Data Collection System(MDCS)
  ‥openXdata: OSS project
  ‥Nokia Data Gathering
  ‥Java Rosa
・実装上のchallengesは以下の4点
 ‥Cryptography  APIの選択/実装
 ‥鍵生成
   mobile deviceには十分なentropy源もないし、そもそもAPIもない。サーバ側で生成する
 ‥Secureなデータアップ/ダウンロード
 ‥Secureなストレージ
・Nokiaの(かなりチープな)携帯電話での実装/性能評価結果


■Application-Replay Attack on Java Cards: When the Garbage Collector Gets Confused Guillaume Barbu, Philippe Hoogvorst and Guillaume Duc(Institut Telecom/Telecom ParisTech)
・Java Card Securityにおけるアプリケーションインスタンス削除について、
  JC 2.2.2 SpecとJS3.0.1 Specの記述の違いから、セキュリティホールが発生する恐れ
 ‥オブジェクトが存在するが、そのアプリケーションインスタンスが削除されたもの。JC3.0.1ではGCが走るまで削除されない。
 ‥オブジェクトへの参照を外さないことで、GCによる回収を防ぎ、削除させないようにする


■Plagiarizing Smartphone Applications: Attack Strategies and Defense Techniques
 Rahul Potharaju, Andrew Newell, Cristina Nita-Rotaru and Xiangyu Zhang(Department of Computer Science, Purdue University)
・Smartphone用の"パクリ"アプリケーションについて。著名なゲームアプリAngry Birdsの剽窃版の紹介
・これまでの大半の対策はクライアント側によるもの
  ‥情報漏洩の検知    TaintDroidの研究
  ‥アクセス制御のリッチ化   NAumanら。Apex
  ‥ Google Bouncer 2012
  オリジナルのアプリからfeature vectorを抽出
    Dex Dump -> Code transformation -> AST構築 -> Feature Extraction


セッション: Trust
座長: Sandro Etalle
■A Task Ordering Approach for Automatic Trust Establishment
 Francisco Moyano, Carmen Fernandez-Gago, Isaac Agudo and Javier Lopez
  (Department of Computer Science, Univ. of Malaga)
・a prioriの状態から、どのようにしてinitial trustを確立するか
  ‥タスクにはorderが存在する。例えば、read taskとwrite taskの間
・複数エンティティ間のあるタスクに関するトラストを、重み付双方向グラフで表現
    タスクについての重ね合わせで、重み付きmultigraphが構築される。
    タスクの順序付けのプロセスは、リスクアセスメントプロセスとなる。
・TIV: Trust Incremental Value(1より大きい)を用いた定式化
・e-health systemへの適用を目指すが、実装はこれから


 ■Security Policy Conflict Detection
 Matteo Maria Casalino, Henrik Plate and Slim Travbelsi(SAP Labs, France)
・通常のポリシイ解析のアプローチは、だいたい単一のポリシイクラスをターゲットにしている。しかしtraversal conflictが発生しうる。何故発生するのか?
  ‥ポリシイが独立に決定されている
  ‥異なるポリシイランゲージ間のセマンティックギャップ
  ‥アプリケーションドメインの依存性の強さ
・ロジックフレームワークの構築
   ‥Domain Description Model(DDM)
   ‥Class-Specific Policy Models(CSPMs)
   ‥Conflict Specification Model(CSM)
     Transversal conflict検知はCSMのSAT(充足可能性)検査で実現


Keynote2:An Overview of Modern Security Threats
Thorsten Holz(Univ. of Manheim)
・APT: Advanced Persistent Threat
 クラッカー集団LulzSec対Sonyの暗闘の例
 洗練されているとは限らない
・Stuxnetの脅威について
  高度に洗練された攻撃
  合衆国がスポンサード?
・Spam
   我々が直面する最も面倒な問題の一つ
   Rustock: 最も大きいボットネットの一つ。SPAMの30% March 2011にtakedown
   30.3%のみが実際にデリバリされている
    正しくないメールアドレス  53.3%
    SMTPブラックリスティング  16.9%
    種々のSMTPエラー        11.8%
    コネクションタイムアウト 11.3%

・サマリとして
 APTは多くの企業をリスクにさらす。しかし幾分hype気味である
 攻撃はカネになる。経済学的側面は興味深い
 Workshop on the Economics of Information Security(WEIS)


セッション: Models and policies
座長:Thorsten Holz(Univ. of Manheim)
■Supporting the Development and Documentation of ISO 27001 Information
 Security Management Systems Through Security Requirements Engineering
 Approaches
 Kristian Beckers, Stephan Fassbender, Maritta Heisel(Univ. of Duisburg-
 Essen),Jan-Christoph Kuster and Holger Schmidt(Fraunhofer Institut for
 Software and Systems Engineering ISST)
・ISO 27001(ISMS)準拠の困難さ(の一部)は、システムサポートの不備に由来する。
・Security Requirement Engineering(SRE)メソッド
  セキュリティ要件の抽出と分析の方法
  SREメソッドとISO 27001の対応付け


■An Independent Validation of Vulnerabilities Discovery Models(Idea Paper)
 Viet Hung Nguyen and Fabio Massacci,(Universita degli Studi di Trento)
・ソフトウェアのVulnerability Discovery Model(VDM)、既存のものは
 ‥Rescorla Quadratic(RQ)
 ‥Rescorla Exponential(RE)
 ‥Alhazmi-Malaiya Logistic(AML)
 ‥Anderson Thermodynamic(AT)
 ‥Linear model(LN)
 ‥Logarithmic Poisson(LP): Musa-Okumoto Model
 どのVDMが機能し、どれが機能しないか。
・ブラウザ17リリースを対象に、上記VDMを評価
 ‥Goodness of Fit(GoF)解析

■A sound decision procedure for the compositionality of secrecy(Idea Paper)
Martin Ochoa, Jan Jurjens and Daniel Warzecha(Software Engineering, TU Dortmund, Fraunhofer ISST, Siemens AG)
・攻撃者のDolev-Yaoモデル
・Compositionにおけるセキュリティの保持
・First Order Logicを用いたプロトコル検証テクニックの応用
・TLS(の古いバージョン)を例に解析


セッション: Applied cryptography
座長: Gilles Barthe
■Typed Assembler for a Crypto-Processor
  Peter Breuer(Dept. of Computer Science, Univ. of Birmingham),
  Jonathan Bowen(Faculty of Business. London South Bank Univ.)
・Crypto-Processorとは
 ‥暗号化されたデータと、平文データをmixして処理可能な、RISC proc.
  runs safely in emulation on standard hardware
  runs existing machine code(once encrypted)
  しかしプログラムアドレスは暗号化できない。
・デザインの詳細はNDAなしでは公表できない。
・Robin Milnerの型理論に基づく型推論

■Design of Adaptive Security Mechanisms for Real-Time Embedded Systems
  Mehrdad Saadatmand, Antonio Cicchetti and Mikael Sjodin(Malardalen
  Real-Time Research Centre(MRTC))
・リアルタイムシステムにおける、セキュリティとタイミング要求の両立。システム
  の複雑性が増すにつれ、コンポネントのタイミング上の振る舞いの解析が困難
・OSE RTOS
  ENEA開発の分散RT OS
・RT性の要求に従い、暗号アルゴリズムのスイッチ


ページトップへ戻る

Copyright © 2004-2012 Institute of Systems, Information Technologies and Nanotechnologies. All Rights Reserved.