[B! FormalMethod] notaeのブックマーク

プログラム中の文字列チェック機能の脆弱性を自動修正する技術を世界に先駆けて実現～専門知識をもたない開発者でもReDoS脆弱性の修正が容易に～ | ニュースリリース | NTT

日本電信電話株式会社（本社：東京都千代田区、代表取締役社長：澤田　純、以下「NTT」）と学校法人早稲田大学（本部：東京都新宿区　理事長：田中愛治　以下、「早稲田大学」）は、文字列のチェック機能の処理時間を長期化させコンピュータの負荷を大幅に増大させる攻撃を引き起こす脆弱性に対する実用的な自動修正技術を世界に先駆けて実現いたしました。文字列のパターンマッチに用いられる正規表現（※1）とは、特定の文字の並び（文字列）をルールに基づき簡略化して表現する方法で、Webサービスなどにおいてユーザの入力値が期待したものであるかの検証など幅広い場面で利用されています。難解な正規表現の仕組みやルールを深く理解し、検証すべき文字列を厳密に定義できていないと脆弱性になってしまうため、近年グローバルで大きな脅威となっています。この技術によって、専門知識をもたない開発者でもこうした正規表現の脆弱性の修正が可能とな

notae 2022/03/23

リンク

CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech Festa 2021 winter

July Tech Festa 2021 winter で使用したスライドです。バグのない分散システムの設計は果たして可能でしょうか？この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。形式手法はシステムの挙動を数学的に解析する技法で、「ノードが特定のタイミングで故障した場合にのみ発生するバグ」といった再現困難な問題を確実に検出することができます。本講演では、CockroachDB の事例を通して、形式手法が実世界で活用されている様子をお伝えします。イベント概要：https://techfesta.connpass.com/event/193966/ ブログ記事：https://ccvanishing.hateblo.jp/entry/2021/01/24/185819 録画：https:/

notae 2021/01/24

リンク

AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計

NGK2015B で使用したスライドです。モデル検査器 Alloy を用いて、AWS のセキュリティグループ設定を自動で検査します。Read less

notae 2016/01/03

リンク

あるソフトウェア工学者の失敗日本のITは何故弱いか

このドメインはお名前.com から取得されました。お名前.com は GMOインターネットグループ(株) が運営する国内シェアNo.1のドメイン登録サービスです。 ※表示価格は、全て税込です。 ※サービス品質維持のため、一時的に対象となる料金へ一定割合の「サービス維持調整費」を加算させていただきます。 ※1 「国内シェア」は、ICANN(インターネットのドメイン名などの資源を管理する非営利団体)の公表数値をもとに集計。gTLDが集計の対象。日本のドメイン登録業者(レジストラ)（「ICANNがレジストラとして認定した企業」一覧（InterNIC提供）内に「Japan」の記載があるもの）を対象。レジストラ「GMO Internet Group, Inc. d/b/a Onamae.com」のシェア値を集計。 2023年5月時点の調査。