すごｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ
情報漏洩が起きないことを数学的に保証するバックエンドフレームワーク「Nyxis」を公開しました！
たぶん世界初です。
Nyxisで書かれたバックエンドは、企業の持つ機密情報をより安全に守ることができます。
昨今急増しているサイバー攻撃を防ぐ手段として、このような方法があることをお伝えしたいと思い、今回の発表に至りました。
開発者は「どの権限を持つユーザーが何を実行可能であるか」のルールを管理するだけで、残りのコードをAIエージェントに任せても認可の安全性が担保されます。
Nyxisは大部分がLean言語で記述されており、形式検証によって
「任意のHTTPリクエスト列に対し、認証された主体の正当な権限を逸脱するデータの読取・変更・削除・権限付与は発生しない」
という認可安全性定理を機械的に証明しています。
認可の不備は、OWASP脆弱性ランキングにおいて2019年版から連続1位であり、最優先で対策すべきリスクの一つです。
形式検証を活用したこのフレームワークは、テストに頼る従来の開発に比べて、格段にセキュアなソフトウェアを実現します。
先日MicrosoftとGitHubが、形式検証を用いた開発キット「PDD Kit」を発表しました。
こちらはより幅広い性質を扱える一方、プログラムごとに仕様を作り、それが意図に合っているかを開発者が確認する必要があります。
Nyxisは証明する定理を認可安全性に絞ってあらかじめ定めているため、開発者はポリシーを管理するだけで済みます。
もちろん、一定の仮定は存在しています。証明外コードと実行環境は信頼する前提であり、開発者がポリシーを誤って書けば、意図した保護は得られません。
この定理の範囲内において、数学的保証は非常に強力です。実システムに組み込める技術としてここまでの保証を与えたものは、私の知る限りまだ存在しません。
一方で、表現力の乏しさやLeanのライブラリ不足など、改善すべき点はまだ山積みです。
本当はもっと完成度が高まった時点で公開しようと考えていましたが、昨今のセキュリティインシデントの状況を鑑みて、このタイミングで発表することにしました。
世界をセキュアにする一助になれば嬉しいです。
github.com/NyxFoundation/nyx…
askyv retweeted
人が熱くなる時って
「参加している文脈が強化、肯定された瞬間」
「新しく文脈が見つかる瞬間」
「継承された時」
が、基本的な条件だから、人を熱くしてれば絶対に自分の人生も熱くなるし、
不思議なことに、なんなら新しい文脈も見つかるんだよ
askyv retweeted
ついにふるさと納税の制度を使ってNyxの活動を応援できるようになりました！
個人の方であれば富山県南砺市の返礼品がもらえますし、税控除もあります。企業も返礼品はないですが応援可能です！
今回の寄付の使い道や目指している方向性は下のプレスで書いたのでぜひ！
【お知らせ】
Nyx Foundationが提案した事業が、富山県南砺市のふるさと納税を活用した補助対象事業に採択されました！
これにより、ふるさと納税を通じて、私たちの挑戦を応援いただけるようになりました。
・AIで伝統工芸の新しい用途やデザインを3Dモデル化
・SNSで需要を検証し、職人との作品づくりへ
・技術や実証結果をオープンに公開
研究所「Nanto」構想の第一歩として、研究を地域の未来につなぐ取り組みを始めます。
目指すのは、研究成果が新しい産業や仕事を生み、人や資金が集まり、さらなる挑戦につながっていく町。
豊かな自然や伝統文化とテクノロジーが共存する、次世代のまちづくりを南砺市から実現していきます！
prtimes.jp/main/html/rd/p/00…
