OpenSSL #ccsinjection Vulnerability
[English] 最終更新日: Mon, 16 Jun 2014 18:21:23 +0900 CCS Injection Vulnerability 概要 OpenSSLのChangeCipherSpecメッセージの処理に欠陥が発見されました。 この脆弱性を悪用された場合、暗号通信の情報が漏えいする可能性があります。 サーバとクライアントの両方に影響があり、迅速な対応が求められます。 攻撃方法には充分な再現性があり、標的型攻撃等に利用される可能性は非常に高いと考えます。 対策 各ベンダから更新がリリースされると思われるので、それをインストールすることで対策できます。 （随時更新） Ubuntu Debian FreeBSD CentOS Red Hat 5 Red Hat 6 Amazon Linux AMI 原因 OpenSSLのChangeCipherSpecメッセージの処理に発見
Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何
スマートコン @mr_konn Haskell における依存型プログラミングでは、大抵の場合安全性の"証明"として依存型を用いる場合が多いから、ひとたび証明が出来てしまえば、その証明に対応する実行時計算は無駄なんだよなあ。type erasure ならぬ proof erasure が出来ればよいのだが 2014-02-23 17:10:29 スマートコン @mr_konn 帰納法は O(n) 書かるし、二重帰納法なら O(n^2) だ。一回示せたら unsafeCoerce すりゃいいかもしれないけど、そういうのを自動的にやってくれるのを欲しい 2014-02-23 17:12:45
『ソフトウェアの基礎』のePub版を公開しました。 - みずぴー日記
「Software Foundations(和訳: ソフトウェアの基礎)」はBenjamin Pierce氏らによって書かれたドキュメントであり、Coqによりプログラミングやプログラミング言語の理論が解説されています。基本的な部分から丁寧に解説されているため、Coqの入門書としてもプログラミング言語理論の入門書としても、非常に優れた内容となっています。 今回は、その「ソフトウェアの基礎」のePub版を公開しました。 対応したリーダを用いることで、iPhoneやiPad、Androidで本ドキュメントを読むことができます。 ダウンロード http://proofcafe.org/sf-beta/ からダウンロードできます。 またmobi版もありますが、Kindleを持ってないので、動作確認はしていません。 バグ報告 http://github.com/sfja/sfja へのissues登録
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Coq Party - rfなブログ
11/27 に、Coq Partyに参加してきました。 資料などはこちら。 エンジニア・ミーツ・Coq すぐ分かる形式手法 形式手法とは？ 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法 仕様化の正しさは終盤のシステムテストまで分からない 結合テストでバグが「こんにちは！」 手戻りコストがとても大きい V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」 ソフトウェア開発の不具合の半数は上流工程 その半分は下流工程まで見つからない 上流時点で「厳密で、間違い、漏れ、抜け、矛盾の無い仕様」が必要 仕様は自然言語で書かれているため、あいまい or/xor 問題や、if/iff 問題 など 自然言語ではなく、形式的な仕様記述が必要 形式手法 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う 数学ベースの厳密な定義 形式仕様は仕様の記述の形式化 プログラムではな
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation
イベントレポート：「Coqチュートリアル#1」
名古屋Ruby会議で「Coq to Rubyで初める証明駆動開発」というタイトルで発表してきました - みずぴー日記