Developers Summit 2020 で使用したスライドです。 言葉というものは曖昧です。複数人が「ともにつくる」システムにおいて、メンバ間で仕様を正しく共有することは非常に重要ですが、一方で言葉の裏側に隠された「暗黙の仮定」を見抜くことは簡単ではありません。このような仕様の曖昧性への対抗…
Developers Summit 2020 で使用したスライドです。 言葉というものは曖昧です。複数人が「ともにつくる」システムにおいて、メンバ間で仕様を正しく共有することは非常に重要ですが、一方で言葉の裏側に隠された「暗黙の仮定」を見抜くことは簡単ではありません。このような仕様の曖昧性への対抗…
#45 – Why Amazon Chose TLA +
仕様検証言語 TLA+ の AWS における使用事例について向井が話します。感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。 Why Amazon Chose TLA + | SpringerLink (Google Scholar) How Amazon Web Services Uses Formal Methods Practical TLA+: Planning Driven Development: Hillel Wayne Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers: Leslie Lamport TLA+tlaplus/tlaplus: TLC is an explicit state
AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる 以下は、読んでいる途中で書きだした要点。 AWSでは2011年以降形式仕様とモデル検査を使用している 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレス
I’m a fan and long-term user of the Isabelle/HOL proof assistant. More recently I have been studying Lamport’s TLA+ system which is a popular choice for writing specifications of systems. This post is a slightly tidied-up version of some notes about my early experiences of playing with the implementation of TLA within Isabelle/HOL, to record a handful of obstacles I hit and some techniques I found
index : kernel/git/cmarinas/kernel-tla.git Kernel TLA+ specsCatalin Marinas aboutsummaryrefslogtreecommitdiffstats BranchCommit messageAuthorAge masterasidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskCatalin Marinas3 years AgeCommit messageAuthorFilesLines 2021-09-10asidalloc: Fix inadvertently removed line from UniqueASIDActiveTaskHEADmasterCatalin Marinas1-17/+19 2021-08-05asid
オンラインバンキングやオンラインショッピング、その他の慎重を要する接続を暗号化し、盗聴を阻止するために利用されている暗号化プロトコル TLS に対する新しいマンインザミドル攻撃を、セキュリティ研究者たちが開発した。 この「Triple Handshake」と呼ばれる攻撃は、特定の条件下において、「安全性の高い接続方法でサーバに接続するユーザー」の身元を確かめるのに不可欠な確認作業の裏をかくことができる。 言い換えるなら、悪質なシステムがユーザーのログイン認証情報（この場合はクライアント証明書）を傍受することにより、それと同じ認証情報を許可するあらゆるサーバで犠牲者になりすますことが可能となる。 この新たな欠陥は、フランス国立情報学自動制御研究所（INRIA）のセキュリティ研究者たちによって発見されたもので、この業界にいる彼らがこれまでの仕事から描き出したものだ。
& www.cea.fr C2TLA+: A translator from C to TLA+ Amira METHNI (CEA/CNAM) Matthieu LEMERRE (CEA) & Belgacem BEN HEDIA (CEA) Serge HADDAD (ENS Cachan) & Kamel BARKAOUI (CNAM) June 3, 2014 Cliquez pour modifier le style du titre DACLE Division| June 2013 © CEA. All rights reserved | 2 & Outline Introduction General approach Translation from C to TLA+ Memory model Expressions Intra-procedural control
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
