jagijagijag1 / article-paper-summary

summarize articles/papers I read as issues

Hi there 👋

metrics (by lowlighter/metrics)

my daily stress (by Pixela & Garmin Connect = GarminStress2Pixela)

article-paper-summary's Issues

On serverless, data lock-in and vendor choice

リンク

On serverless, data lock-in and vendor choice

抜粋・メモ

• vender lock-inのキモはdata lock-in
  • e.g. Lambdaを使おうと思うとS3などのAWSサービスとの連携が強制される→データをAWSに置かざるを得ない
  • これを回避するためにはdata portabilityが重要
• data portabilityに向けてはOSSの活動あり
  1. CloudEvents (CNCF): サービス間のイベント形式の標準化活動
  2. Event Gateway (serverless): イベントをあるサービスから別サービスへルーティングする機能を提供

On serverless, data lock-in and vendor choice

リンク

On serverless, data lock-in and vendor choice

抜粋・メモ

• vender lock-inのキモはdata lock-in
  • e.g. Lambdaを使おうと思うとS3などのAWSサービスとの連携が強制される→データをAWSに置かざるを得ない
• これを回避するためにはdata portabilityが重要
• data portabilityに向けてはOSSの活動あり
  1. CloudEvents (CNCF): サービス間のイベント形式の標準化活動
  2. Event Gateway (serverless): イベントをあるサービスから別サービスへルーティングする機能を提供

Formal Reasoning About the Security of Amazon Web Services

著者/所属機関

Byron Cook (Amazon Web Services, University College London)

出典

FLoC 2018 (CAV 2018)

• FLoC Plenary Lecture (CAV 2018 Invited Paper)
  • AWSでの形式手法の活用について
  • Open Accessのため↓で閲覧可能
    • Formal Reasoning About the Security of Amazon Web Services | SpringerLink
  • 講演の映像も↓から視聴可能
    • Formal Reasoning about the Security of Amazon Web Services | University of Oxford Podcasts - Audio and Video Lectures

内容

• AWSでは分散アルゴリズムの設計に形式手法(TLA+)を使用 (2014)
• 本論文では特にAWSでのセキュリティに形式手法を用いた事例を紹介

Security of the Cloud: Where Formal Reasoning Fits In

• AWS内部の開発，特にセキュリティレビューで定理証明やモデル検査(symbolic model checking)の利用が増えている
• 2017年だけでも下記の事例にて定理証明やモデル検査を適用
  • s2n (TLS/SSL実装)の検証
    • ちなみにこの内容の論文が同会議にて発表されている
    • Continuous Formal Verification of Amazon s2n | SpringerLink
  • ハイパーバイザ，ブートローダ，BIOS，ファームウェアの検証
    • こっちも同会議で発表あり
    • Model Checking Boot Code from AWS Data Centers | SpringerLink
  • ガーベッジコレクタ
  • ネットワーク設計
• OSSを活用しつつ使う上で生じた変更をフィードバックしており，例えば下記を利用+貢献
  • CBMC: C/C++向けのbounded model checker
  • SAW: CやJabaでの特定性質の検証
  • SMACK: Cプログラムに対するアサーション検証
• s2nなど一部プロジェクトでは形式検証ツールをCI/CDに組み込み，継続的検証を実施
• SMT-basedのツールで設定ミス防止を図っている
• 形式手法の利用はコードを書く前から始まっている＝プロトコルやアルゴリズムの設計段階から利用

Securing Customers in the Cloud

• AWS利用者側に対しても形式手法の適用が始まっている
  • 例えば，S3の公開設定ミスを警告する機能をSMTソルバを用いて実現
    • おそらく↓の話
    • How AWS uses automated reasoning to help you achieve security at scale | AWS Security Blog
  • AWS Macieでも同様のツールを利用
  • 複雑なネットワーク設定時の到達性(おそらくルーティングや通信可否)をdatalogを用いて検証

その他

• 他社事例(文献)として以下に言及 (抜粋)
  • IBM, Google @ Dagstuhl Seminar 2013
  • Microsoft @ SOSP 2015 分散システムの検証
  • Facebook @ LICS 2018 codebaseの継続的検証

Challenges

• Reasonign About Risk and Feasibility: セキュリティエンジニアは大半の時間を"informal"なリスク分析に使ってる→Formalにしていきたい
• Fixes Not Findings: 見つけるだけじゃなく直し方まで合わせて自動化していきたい (synthesis技術など)
• Auditable Proof Artifacts for Compliance: mechanical proofでチェックできる部分もある
• Tracking Casual or Unrealistic Assumptions: 形式手法を使う時点でなにかしかの過程をおいているので注意
• Distributed Formal Verification in the Cloud: 検証問題を自動で分割して並行実行する手法はまだ十分に研究されていない
• Continous Formal Verification: システムのデプロイ前に最初のproofを見つけるのにかかる時間や労力は，その後proofをメンテする時間やコストと同等=1回使い切りでなく，継続的な利用が重要
• The Known Problems are Still Problems: AngularやLinuxといった巨大なシステムのセキュリティ検証は解決済みとは言えない，分散・並行システムの検証手法も未だにopen problem

How AWS uses automated reasoning to help you achieve security at scale | Amazon Web Services

リンク

How AWS uses automated reasoning to help you achieve security at scale | AWS Security Blog

抜粋・メモ

• AWS Configで指定したルール(IAMやS3のポリシ設定)検証をSMTソルバベースの技術(Zelkova)を用いて検証
  • e.g. S3ポリシを見て，publicアクセスが可能な設定になっていないか検証
  • パターンマッチングやシミュレータではなく"証明"
• AWS側で内部的に定義したルールへの違反を検証している様子
  • 任意のルールを定義して検証させることはできない
  • 企業には提供している?

Model-Driven Elasticity for Cloud Resources

著者/所属機関

Hayet Brabra (Universite Paris-Saclay) et al.

出典

CAiSE 2018

目的

クラウド上で動作するアプリケーションの動的リソース割り当て(elasticity)を表現・定義する

問題

既存手法(AWS CloudFormatinや各種研究)での記法はLow-levelなため直感的でなく，ベンダ依存

解法

ステートマシンベースでリソースへの抽象的操作を記述可能なモデルを提案

結果

ユーザ実験にて17%の作業時間削減
またTOSCA, CloudFormationで実現されたユースケースを提案モデルで表現可能なことを確認

備考

Applying principles of chaos engineering to AWS Lambda with latency injection

リンク

Applying principles of chaos engineering to AWS Lambda with latency injection

抜粋・メモ

• Latencyのスパイクは不可避 (AWSの領分で制御不可）
• API Gatewayは29秒のタイムアウトあり (Lambdaが5分まで処理できるがそれとは別)
• Latencyの挿入箇所
  1. HTTP client libray (or 3rd party lib)
     関数のタイムアウト設定とハンドリングの確認可能．また3rd partyサービスへも適用可能(e.g. AWS SDK)．
  2. 内部利用される関数
     特に中間サービスに適用すると，依存する全サービスのタイムアウト処理を確認可能
  3. クライアントに直結する関数
     1クライアント側のタイムアウト処理を確認可能
• Latencyの挿入の観点
  1. どの操作にdelayを入れるか
  2. どの程度の頻度で，どの程度の長さのdelayを入れるか
• HTTP ClientへのLatency挿入
  1. アスペクト指向アプローチ (静的言語)
  2. 動的プロキシを使う (静的言語)
  3. wrapperを作る
• AWS SDKへのLatency挿入
  • factory functionを使う (e.g. Getting Started | bluebird)
• 関数起動へのLatency挿入
  • これもfactory functionで実現

Centralised logging for AWS Lambda, REVISED (2018)

リンク

Centralised logging for AWS Lambda, REVISED (2018) | theburningmonk.com

抜粋・メモ

• 関数実行したログを関数で転送などの処理すると，並行実行する関数の数が倍になるので注意
• Kinesisのストリーム処理する方がベター (Kinesisで流量制御)
  • CloudWatch Logs -> Kinesis -> Lambda

Debugging with intelligence via probabilistic inference

リンク

Debugging with intelligence via probabilistic inference

抜粋・メモ

• Debugging with intelligence via probabilistic inference Xu et al., ICSE’18
• "We model debugging as a probabilistic inference problem"
  • 直感的には
    1.人が各ステートメントにエラーっぽさのスコアをつける (よくわからなければとりあえず0.5とかもあり)
    2.ツールが変数などを追っかけてエラーっぽさのスコアを更新
    3.1と2を繰り返す → 数回のインタラクションで不具合の原因を見つけられた

7 Essential DevOps Tools to Maintain Serverless Operations - The New Stack

リンク

7 Essential DevOps Tools to Maintain Serverless Operations - The New Stack

抜粋・メモ

• Dashbird
  • AWS Lambdaの監視&デバッグプラットフォーム
  • Serverless Performance Monitoring & Debugging Tool - Dashbird
• Stackery
  • リリース管理
  • Stackery | Serverless Development for Teams
• Thundra
  • for observability
    • データ収集機能のコード断片を自動追加
    • 非同期に収集するのでオーバーヘッドなし
  • Thundra | Serverless Observability

Reservationパターンを使ったSOAトランザクション

リンク

Reservationパターンを使ったSOAトランザクション

抜粋・メモ

• Sagaパターンを使う主な理由は、サービスをまたいだトランザクションを利用しないようにするため
  • ロールバックを行うことができないので、代わりにインタラクションの操作を逆向きにした取り消し操作により、擬似的なロールバック処理を行う
• 補償とSagaパターンの他の制限事項：外部のコーディネータが必要となり、それによってサービスと外部のコーディネータとの間に望まざる結合が生じてしまう → Reservationパターンの提案
  • 予約依頼が来たとき，予約情報を書き込む＋注文確認が到着するまでのタイマもしくは有効期限を設定する。あるいは注文が最終決定していないことを示す目印を設定する。
  • 確認が来たら最終確定，それまで他の依頼に渡さない．期限が切れても確認が来なければ破棄．
  • 最初のパスでは、プロセスを開始したものが、各参加者に予約を行うように依頼する。もし全ての関連するサービスから（タイムアウト時間以内に）OKと受け取ると、2つめのパスを始めて、すべての参加者に予約確認を行う。

Localizing Faults in Cloud Systems

著者/所属機関

Leonardo Mariani (Universita degli studi di Milano Bicocca) et al.

出典

ICST 2018

目的

クラウド上で動作するアプリケーション(役割ごとのサーバ/VMで動作する
分散アプリケーション)におけるfault localization

問題

既存手法は，意図的にfaultを入れ込んだ状態でのアプリケーションの動作を
学習させる必要があり，準備コスト高

解法

正常状態の学習のみで，異常状態の検出＋異常の発生源を特定する手法を提案

• 正常状態でのKPI(サーバXでのCPU使用率など)を学習し，KPI間の結びつきをcausality graphとしてモデル化
• causality graphと比較し，現状のKPI(メトリクス)が異常値か判定
• 異常状態を検知した場合，異常状態にあるKPIをcausality graphから抽出 (=propagation graph)
• propagation graphに対してgraph centrality algorithms (Page Rank algorithmなど)を適用し，fault原因を特定

結果

OSSのIP Multimedia Subsystemに意図的にfaultを入れ，当該faultを
特定可能か評価し，既存手法(faultを入れ込んで学習する手法)と同等の性能
を，少ないオーバヘッドで達成することを確認

備考

How can we apply the principles of chaos engineering to AWS Lambda?

リンク

How can we apply the principles of chaos engineering to AWS Lambda?

抜粋・メモ

• AWS LambdaにはEC2に対するものとは違った障害モデルが必要
  • EC2へのChaos Eng.では"このインスタンスが居なくなったらどうなるか"が中心
• Lambdaの呼び出し失敗時，リトライ起動時の動作，Kinesisのポーリングなど，それぞれに対して障害を考える必要あり
  • 異常を誰がキャッチするかの検討も必要

Fear the reaper: characterization and fast detection of card skimmers

リンク

Fear the reaper: characterization and fast detection of card skimmers | the morning paper

抜粋・メモ

• ATMなどの磁気カードのスキミング手法で，カード挿入口のカバー部分にスキミング機器を仕込む手法がある
  • 一緒にカメラを仕込んで暗証番号を押すところを撮影
• スキミングがあった場合には2度のカード読み込みが起きている→カード読み込み状態を調べ，想定よりも多くの回数の読み込みがあったかどうかでスキミング検知する手法を提案

Finance: State of the Cloud 2018

リンク

Finance: State of the Cloud 2018 - CloudCheckr

抜粋・メモ

• 2017のAccentureの調査によると，82%の金融機関がすでにパブリッククラウドを何らかの形で使用している
  • リンクが設定されていないので引用元不明
• Capital OneはAWSを最も活用しているところの一つ
• J.P.Morganは2017年に3つのコアアプリをパブリッククラウドで立ち上げた
  • うち2つはtrading関係，3つ目はリスクモデリング
  • J.P. Morgan Set to Run First Apps in Public Cloud - CIO Journal. - WSJ
• イノベーションのスピードが上がるのが導入理由の第一位
• データについてはオンプレのデータセンタよりパブリッククラウドに置くほうが安全
• McAfeeの調査によると，クラウド上でのデータセキュリティを確保するベストプラクティスがパブリッククラウドで提供されている
• 金融機関はcloud-nativeなプラットフォームに適応しなければならない
  • 特に，Hybridなマルチクラウド環境

Testing Cloud Applications under Cloud-Uncertainty Performance Effects

著者/所属機関

Wei Wang (University of Texas) et al.

出典

ICST 2018

目的

マルチテナントなクラウド上でのアプリケーション性能保証

問題

マルチテナント環境では予測困難な性能のブレ(Uncertainty)が生じるため，
ブレの影響を含めて性能保証するためには長期間のテストが必要となり，
クラウド利用コストが嵩む

解法

下記手順を通じ，クラウド上での性能予測および性能要件を満たすか判定する手法を提案

1. micro benchmarkを用いてクラウド上のリソースの性能のブレを測定・モデル生成
2. ローカル実行結果とクラウド上でのサンプリング実行結果とを用いて対象アプリケーションのベースライン性能を導出
3. 1，2の結果と，性能要件(e.g.95%の割合で実行時間120秒を超えない)を入力に，要件を満たすかを判定

結果

Chamelon cloudとAWSにて7種類のアプリケーションを評価し，
手法による性能予測と実測とのズレが4.9%であること，
手法適用時のクラウド利用コストを66.9%削減することを確認

備考

2018 Serverless Community Survey: huge growth in serverless usage

リンク

2018 Serverless Community Survey: huge growth in serverless usage

抜粋・メモ

• serverlessで直面している課題
  • managing and enforcing best practices
  • lack of tooling
  • lack of knowledge on their team
• サーバレス開発で一番課題になる工程
  • debugging, monitoring, & testing
  • -> すべてツール不足に起因

Serverless Security Risks Laid Bare

リンク

Serverless Security Risks Laid Bare - The New Stack

抜粋・メモ

• serverless platfromはワークロードをよりセキュアにする
• コンテナがOS, ハード層の保守・セキュリティ担保の分離を実現した → サーバーレスはアプリとWebサーバの層に対して同じことを実現する
• サーバーレスアプリの場合，最も一般的な攻撃はSQLインジェクション
• アクセスコントロールに関する2つのリスク
  1. アプリ側が何らかのアクセス権を持っている→どこまで許容するかの設計が問題
  2. 開発者が楽するために，アプリに必要以上のアクセス権をもたせるケース