「クラウドを支えるこれからの暗号技術」を読んだ
「クラウドを支えるこれからの暗号技術」は上の紹介記事にもあるように最近の暗号技術についてのドキュメントで、無料で公開されている。
自分は体系立って暗号技術を学んだことがないので、何かいい本ないかな〜と思っていたところでドキュメントが公開されたので読んでみた。読んだといっても、1部「暗号の基礎」2部「新しい暗号技術」3部「数学的なはなし」と分かれている中で、1部2部で省略された数学的な部分の穴埋めをする3部は読んでいない。
最近の暗号技術を説明するという内容だけど、1部は楕円曲線暗号を含めた基礎をしっかり説明しているし、知らない人は1部だけ読んでみても十分面白いと思う。紹介記事に「入門書と専門書の合間を埋める目的で書かれました」と書かれているように、もうちょっと踏み込んで知りたいという人にとっては、難しすぎもせず少な過ぎもせず満足できる内容でした。このように丁寧に書かれたドキュメントが無料で読めるというのは素晴らしい。
メインとなるであろう2部はクラウドサービスが普及しているなか、全面的にサービスを信用しているわけではないので、暗号化したままデータを扱うにはどうすれば良いのかという、最近だとニーズがありそうな話が多い。クラウドに関連するものだけではなく、放送型暗号や電子投票についての話もある。面白かったトピックを並べると
- ペアリング
- IDベース暗号
- 準同型暗号
- ゼロ知識証明
がある。
最近、社内で内定者向けに Web アプリケーションセキュリティ周りの勉強会が開かれていて、サポーターとして参加したのだけれど、勉強会で使っているドキュメントがいわゆる徳丸本だった。「体系的に学ぶ 安全な Web アプリケーションの作り方」という徳丸本のタイトル通り、体系的に学べる超良著ではあるが発売が 2011 年ともう 4 年前の本になっていて、それ以降に話題になった話が載っていない(例えばクリックジャッキング)。それで社内のセキュリティ大好きっ子に、いつまで徳丸本だけで勉強しているのかと言われてしまった。
セキュリティ周りの動向は早いので、教えるとき or 学ぶときは体系立ってかつ最近の話も載ってるものを期待するのではなく、既にある良書と他の新しめの情報を組み合わせないといけない。
「クラウドを支えるこれからの暗号技術」は扱ってる内容が最近の話だというのもあるけれど、1部の基礎のところでも POODLE や Snowden の告発と前方秘匿性、Bitcoin の話など、比較的最近の話も絡めている。
暗号技術を体系立って学ぶ本には
- 作者: 結城浩
- 出版社/メーカー: ソフトバンククリエイティブ
- 発売日: 2008/11/22
- メディア: 単行本
- 購入: 46人 クリック: 720回
- この商品を含むブログ (81件) を見る
があるらしいが(まだ読んでない…)、「クラウドを支える〜」の方の紹介記事に「暗号技術入門」には楕円曲線暗号について触れられていないと書いてあるので、徳丸本と同じように良著でも最近の話が載っていないということが起きているのかもしれない(Amazon 商品ページで目次を確認すると楕円曲線暗号については新板の5章に書かれているっぽい)。「クラウドを支える〜」は GitHub で管理されているので、新しい情報もどんどん追加されそう。
おいお前ら、TAPL読むぞ!
こんにちは。VOYAGE GROUP エンジニア blog Advent Calendar 最終日分の記事です。
TAPL(Types and Programming Languages, 型システム入門)を一緒に読もうよという内容になります。
アドベントカレンダー最終日、クリスマス・イブだからおもしろネタ記事かと思った?残念!型システムでした! クリスマスだからって浮かれているようではエンジニアとして生き残れないですぞ!(弊社では社内バーでクリスマスにビールを飲んだり楽器を鳴らしたりしてワイワイする voyarock という会がありますので、興味ある方はぜひ参加してみてください https://atnd.org/events/59995 )
あと、ネタ枠は Slack で役に立たない Bot を運用するときの知見とか - ミントフレーバー緑茶 で勘弁して下さい。
社内読書会について
VOYAGE GROUP では技術書の読書会がいくつかあります。今年参加した/しているものをリストアップしてみると
- SQLアンチパターン勉強会
- @hironomiu の解説付きで、3 周目があるとか
- 参考: http://tech.voyagegroup.com/archives/7759653.html
- ハイパフォーマンス ブラウザネットワーキング輪読会
- 今年の前半に @hagino3000 中心で輪講会がありました
- モバイルアプリケーションの最適化など色々な分野にまたがっていて、参加者の傾向がバラけていていい感じだった
- 参考: http://hagino3000.blogspot.jp/2014/08/hpbn.html
- SICP(Structure and Interpretation of Computer Programs, 計算機プログラムの構造と解釈)輪読会
- プログラムの動作原理を学べる非常に面白い本
- 問題を解いていきながら丁寧に理解していく輪読会で、2 年以上掛かかりましたが最近終わりました
- 2 年掛かってもついてくる人がいるのは、@ajiyoshi のサポートあってこそ
- 参考: http://d.hatena.ne.jp/ajiyoshi/20121226/1356493118
- PRML(Pattern Recognition and Machine Learning, パターン認識と機械学習)輪読会
- @a_macbee を中心に最近始まりました
- 難しいけれどデータ解析周りに興味がある人が多いのか、結構人気(未検定)
と、自分の感覚では質の高い勉強会が開催されています。
最近では上記の勉強会に加えて TAPL 勉強会という、型システムを学ぼうという勉強会を毎週月曜日にやっています。 最初は輪読会のように TAPL のある章を読んで解説するという進め方をしていたのですが、最近の参加者は 2, 3 人で、その少人数で気合入れて資料作ってきてもねぇという雰囲気になり、今はもくもく会の体をとっています。各自で TAPL を好きなように読んで、何かトピックがあればそれについて話すという形です。
以降では TAPL を読む理由や、現在までに自分が 10 章まで読んで学んだことを書きます。取っ付き辛そうと思っている方や、ちょいと割高なので二の足を踏んでるから雰囲気を知りたいと思っている方の参考になったらと思います。
TAPL とは・何が学べるのか
TAPL は型システムについて詳しく解説された本です。動的型付けや静的片付けに関係なく、プログラマなら普段お世話になっている方も多そうな型システムについて理解を深めることができます。
自分が 10 章まで読んで学んだことを箇条書きでまとめると
- 型システムで解決できること
- 型の無い場合はどのような不都合があるのか
- 型無し・型ありラムダ計算器の実装
どういう流れで TAPL を読んでいるか・オススメの読み方
最初は1章・2章・3章…と順番に読んでいましたが順番に読んでいると、証明がよく分からない!自分の頭の悪さよ!!辛い!!!という事態になりがちです(少なくとも自分は)。10 章までの流れだと、定義や証明の多い理論の章=>理論の実装という流れになっており、理論ベースの章に書いてあることを完璧に把握しながら進めるのは難易度が高いかと思います。
幸い実装の章があるので、手を動かしながら全体をゆっくり把握していく学び方が性に合っている方は理論の章を斜め読みした後、実装の方を先にやって、分からないがあったら戻るというやり方がオススメです。実装の章はXXのML実装と書いてある章になるかと思います。
ただし、7 章最後の脚注に「実装したからといって、理解したとは限らない -- Brian Cantwell Smith」とあるように、実装しながら理解すると理解したつもりになって実は間違った理解をしていたとか、実装には現れない部分があったなど「TAPL 完璧に理解した」という状況にはなれないことは気をつけておきたいですね。とはいえ難しい問題や証明があるので、そこで足踏みしたり挫折するなら先に行った方が良い。もしくは「TAPL 完璧に理解した」人に焼き肉を奢ってさっさと教えを請う方が良い(自分の周りには「TAPL 完璧に理解した」人はいないのですが、頭の良い人が多いのが救い)。
各章について(10 章まで)
自分の読んだ 10 章までに書いてある事をまとめます。こっからは個人のチラ裏メモレベルの殴り書きで、TAPL の雰囲気を感じてもらえたらと思います。興味ないとかネタバレ嫌だという方は一気にまとめまで。
1 章 はじめに
TAPL における型システムの定義や、型システムがもたらすものについて書かれている。
型システムとは、プログラムの各部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法
1.1 節「計算機科学における型」より
- プログラムが想定外の振る舞いをしないよう、評価前に検査する仕組みという理解でいる
型システムがもたらすものとして書かれているのは
- エラーの検出
- 抽象化
- ドキュメント
- 言語の安全性
- 効率性
2 章 数学的準備
- 後から分からない部分が出てきたらここで調べる(飛ばした)
3 章 型無し算術式
- 小さな言語を定義することで、構文や評価の表現方法について学ぶ
- 評価は t という状態を t' へ進めると表現できる
- 1 回だけ評価する関係を 1 ステップ評価関係といい (t -> t') で表せる
- もうこれ以上評価できないという状態の項を正規形と呼ぶ
- 正規形は true/false や数値のような値である場合と、値ではないが評価できない場合がある
- 後者は「行き詰まり状態」であり、数値に1を加えるような関数 succ (後者関数) に false を適用したもの succ(false) は、3章で定義された構文では次にどういう状態になるべきか定義されていない
- 行き詰まり状態を実行時エラーとして表すことができる
4 章 算術式の ML 実装
- 型無し算術式を OCaml で実装する
5 章 型無しラムダ計算
- ラムダ計算は関数定義と関数適用を関数だけで表現する
- 項は 3 種類
- 変数 x
- ラムダ抽象 λx.t
- 関数適用 t t
- 例えば、引数をそのまま返すような関数 id への関数適用 id z は (λx. x) zと表現できる
- 項は 3 種類
ラムダ計算は単純ながら、色々な計算を表現できて強力である
- カリー化による複数引数を取る関数の表現
- Church ブール値 true = λt. λf. t
- 2つ組
- Church 数
- 0 の表現 C0 = λs. λz. z
- 1 の表現 C1 = λs. λz. s z
- 後者関数 s を 0 の表現に何回適用したかで n を表す
- 他にも test (if を表現する)、足し算、掛け算、iszero、不動点コンビネータ等
- 表現力はあるけどパズルみたいな複雑さがあって、よくもまあ定義したなあと思う
- (λm. λn. λs. λz. m s (n s z)) (λs. λz. s z) (λs. λz. s (s z)) が1+2 を表してます!というのは自分で考えつく気がしない
後は代入の形式的定義など
6 章 項の名無し表現
- 主に変数の取り扱いについて書かれており、TAPL のラムダ計算では de Bruijn インデックスを用いる
- de Bruijn インデックス
- k 番目に束縛されたときの番号を変数名として利用する
- そもそもなぜこのような名無し表現が必要かというと、変数に名前を付けた場合名前の重複があると実装上ではどの変数(名前無し)を指しているか分からない
- シフトと代入
- 代入が入ると自由変数だった変数が束縛された場合、インデックスの付け替えが生じる
- また、評価(簡約)の場合は変数が消費されるので、これまたインデックスの付け替えが生じる
7 章 ラムダ計算のML実装
- ラムダ計算を実装する
8 章 型付き算術式
やっと型が出てくる
- 4 章で実装した算術式を静的な型で強化する
- 項を評価する前に「行き詰まり状態」にならないかチェックできる
型システムの最も基本的な性質は安全性
- 正しく型付けされた項はおかしくなることがない
- おかしくなるとは行き詰まり状態になること
行き詰まり状態にならないことを進行定理と保存定理によって証明する
- 進行: 正しく型付けされた項は行き詰まり状態ではない
- 保存: 正しく型付けされた項が評価できるならば、評価後の項も正しく型付されている
9 章 単純型付きラムダ計算
- ラムダ抽象に型がつく
- (λx:Bool. x) :Bool->Bool
- Bool を引数にとり、Bool を返す
- 進行と保存の証明とかは長いので飛ばした
10 章 単純型のML実装
- 実装の章(待ってました)
- https://github.com/jewel12/tapl/tree/master/ch10
- パース後に型検査して、評価する
*Main> run "^x:Bool. x"
"(^x:Bool. x) : Bool->Bool"
Bool->Bool を期待されているのに true が引数なので怒られる例。
*Main> run "(^x:Bool->Bool. ^y:Bool. y) true"
"*** Exception: parameter type mismatch
*Main> run "(^x:Bool->Bool. ^y:Bool. y) (^k:Bool. k)"
"(^y:Bool. y) : Bool->Bool"
まとめ
- 弊社には良質な読書会がある
- TAPL を僕と一緒に読もう!
- 人数が少ないので、社内の方でも社外の方でも興味があればぜひ
- クリスマスだからって浮かれているようではエンジニアとして生き残れない(弊社では社内バーでクリスマスにビールを飲んだり楽器を鳴らしたりしてワイワイする voyarock という会がありますので、興味ある方はぜひ参加してみてください https://atnd.org/events/59995 )
VOYAGE GROUP エンジニア blog Advent Calendar 最終日の記事でした!楽しいクリスマスを!
Slack で役に立たない Bot を運用するときの知見とか
この記事は Slack Advent Calendar 2014 - Qiita の 11 日目の記事です。
Slack のようなチャットツールを導入したら Bot を運用するのが人間の性なので、皆さんのチャンネルでも Bot がワイワイ活気付いてる姿が見られるかと思います。 Slack Advent Calendar 2014 - Qiita を眺めていても、Bot の話がいくつかあるようですね。僕が属している会社の Slack チームでも、jewelpet という役に立たない Bot がいます。
今日は Slack で動いている役に立たない Bot の機能紹介と、それを運用して得た役に立たない知見を紹介します。
機能紹介
社内向けなので身内ネタも多い。
jpi
hubot image me
のエイリアスです。hear
を使って jpi
という文字列に反応するようにしています。jewelpet image hoge
よりも短く jpi hoge
と書けるので、画像コミュニケーションが捗ります。
hubot/scripting.md at master · github/hubot · GitHub
社内マップ
会議室の名前と部屋の位置の対応が覚えにくいのでよく使う。
JSON
便利な気がする
返事
鳥
寿司
他にカンパチや太巻きがあります。
ウィキ
コナミコマンド
ジャバ
ガチャ
進捗
いい話カウンター
ユニックスタイムスタンプ
長い
回文
ビール
距離
あなたとダウンロード
優柔不断
コンパイル速度
その他
- 株:
jewelpet 株 CODE
- n 秒後にコメント:
jewelpet timer 10 コンパイル時間
- あとは夕会の通知とかありそうな感じのは大体あります
知見
200 人以上が利用している社内 Slack チームで、鬱陶しいことに上記の様な糞 Bot が運用されていることを紹介しました。
Slack の利用人数が多くなってくると多くの人の目に糞 Bot の糞機能が触れられるようになるため、なるべく角が立たないように運用したくなるかと思います。糞 Bot が運用されている状況を観察して得た知見は、怒られにくくするには愛着がわきやすい Bot を作るのが大切ということです。下手なことを言っても仕方ないと思わせる、そんな可愛さが必要です。
jewelpet には次のような可愛さがあります。
- バグは極力直さない
- バカな子ほど可愛いという諺がある
- 便利な機能は極力付けない
- バカな子ほど可愛いという諺がある
- ChatOps とかもってのほか
- 特定のユーザーしか使えない機能など、あざとい機能もある
この可愛さのお陰で、今のところ怒られずに運用できているみたいです。可愛いは正義!
おまけ: ロギング
役に立たない Bot を運用することの知見からは外れるのですが、Slack で Bot を運用するときはロギング用チャンネルを作って、そこにログを吐いていくと便利です。例えば hubot-cron のようなプラグインを利用するとき、誰が設定した・設定を外したというようなことが分かります。あと検索もできる。
なんか Slack Advent Calendar というよりも Hubot Advent Calendar という感じでしたが、11 日目の Slack Advent Calendar でした。
ISUCON 2014 の思い出
ISUCON 2014 という、いい感じにパフォーマンスチューニングしてスピードアップさせるコンテストの予選に参加しました(詳しくは http://isucon.net/archives/cat_1024989.html)。ポータルに送った時のスコアは 15000 くらいで、一番良かった時は 19000 くらいでした。結果としては惨敗です。
チーム名は「ドラゴンチャーハン」で、@lesamoureuses と @tana_ra と僕が適当に集まって社内チームを組みました。
この記事のまとめとしては、ISUCON 楽しかった!が、惨敗で悔しいので来年も頑張りたい!です。
反省メモ
以下は社内振り返りのために殴り書きしたメモをもう少し読みやすくしたもの。読みにくいと思いますが、来年参加する人の参考になればラッキーです。
予選に向けた練習
ISUCON 2014 夏期講習の AMI を使って練習(去年の予選)しました。
ISUCON 夏期講習 2014 を開催しました : ISUCON公式Blog
2 回集まって練習し、前半はアプリケーションの把握、後半(前日)はチューニング。 前日に Varnish とかを使ってスコアが大きく上がってワイワイしてました。
役割分担
フロントエンドや DB 周りの調整を @lesamoureuses さん、アプリケーション周りでコード書くのを @tana_ra と僕。 このメモはアプリケーション側をいじってた僕の目線で書かれています。
チューニング要点
- Varnish で /mypage をキャッシュしたり、前日に用意していた秘伝のタレ(設定ファイルの調整)をプロファイリング後に入れる
- できるだけメモリに乗っけるようにコードを書き換える
- ストレージが HDD であることと、メモリが 7.5 GB くらいあると聞いた時点で、I/O を発生させないようにする方針になった
- 後述のインテグレーション失敗で全部はできなかった
序盤
- 午前中
- 人数分のインスタンス起動・webapp 以下を Git 管理
- プロファイリングの準備
- Nginx の設定を前日に用意したものに
- LTSV で吐いて、ログを解析しやすくする
- rack-lineprof を入れる
- プロファイリング
- 当然 /report が遅い。 次いで /mypage が遅い
- /report のレスポンスは加点しないということレギュレーションに書いてあったが見落としていたため、ここをチューニングする方針になった
- アプリケーションの理解・戦略を考える
中盤
- 16 時ごろまで
- Redis のセットアップ
- Ruby から Redis を使う方法など変更の方針を共有
- Redis を選んだのは前日に練習で使っていたのと、reds-objects に Redis::Counter というのがあって、ログイン失敗回数をインクリメントしていくのに便利そうだと考えたため(Redis について全然知らなかった)
- 再起動時してもデータの変更内容を保存しておかないといけないことにサポートチャットで気付いた
- Redis に入れてるデータが消えないようにするスクリプトを作成するなどの作業
- 永続化のノウハウが無さすぎた
- ここら辺で /report のレスポンスを高速化する必要がないことに気付く
- アプリケーション側は Redis データ永続化とアプリ変更の2人に分かれた
後半
- 16 時すぎくらい
- 変更済みコードではデバッグが厳しいとわかったので app.rb をまっさらにして、小さい部分から変更していく
- 決断が遅かった
- 残りの時間ないでできることはギリギリまでやって終了
時間があればできたと思うもの
- 主にアプリケーション周り
- SQL を駆逐するつもりしかなかったのでインデックスを張ってない
- 最初にアプリケーション全体に手を加えるという博打をやらずに、インデックス張ったりに手を出してもよかった
知見・反省点
- 中盤まで /report のことしか考えてなかったので、レギュレーションをちゃんと読む。もはやみんなで音読するレベル
- 仕事のやり方みたいな話だが、大きな変更をするときは小さい仕事に分割してちょっとずつ進める
- 実際に3人で本番を想定して練習することがなく、役割分担が不慣れだったということもある
- 練習が足りない
- 前日に Varnish とか Redis を触りだすレベルだったので、もっと持ちネタを増やして望む
YAPC::Asia Tokyo 2014で当日スタッフをしました
去年に引き続き、当日スタッフをしてきました。
YAPC::Asia 2013に参加したです! - ミントフレーバー緑茶
スタッフと言っても例年通りコアスタッフの方々がしっかり準備してくださっているので、椅子を運んだりマイクを運んだりカキ氷を運んだりするくらいであんまり偉そうなことはしません。イベントは準備がキモですね。イベントホールの状況はコアスタッフでウルトラスーパー PHPer であるところの uzulla さんの記事がよくまとめられてて最高です。
スタッフとしてのYAPC::Asia 2014 レポート(Without about my talk) - uzullaがブログ
イベントホールスタッフを 3 グループに分割して、担当部分じゃないところは他のトークを見に行ったら良い。という提案を uzulla さんがしてくださったので、去年よりトークを見る時間ができて良かった。
以下は自分が見た発表&スライドについて。社内で YAPC フィードバック会があるので、もうちょっと発表スライドを読んでいきたい。
「コマンドラインツールについて語るときに僕の語ること」 @deeeet さん
YAPC::Asia 2014でコマンドラインツールについて語ってきた | SOTA
自分にとって目新しいところはなかったけど、スライドがすごく見やすい&分かりやすい。
「オープンソースの開発現場 - Perl 5.20 のSubroutine Signaturesが来るまでの奮闘の軌跡」 @lestrrat さん
YAPC::Asia Tokyo 2014 オープンソースの開発現場 - Google スライド
Subroutine Signatures を追加するまでのドラマが紹介されていた。皆が使っている既存のものに手を入れるということはそれぞれの人にとって賛否両論ある。自分にとっては良かれと思ってやっていることもいろいろな人にいろいろなプライオリティがあるから、否定されることもある。そんな中で自分のやりたいことを実現するには、コードを書いて実装するというだけではなく、やりたいことが実現するように仕向けていく人間力・政治力という、本質的ではなさそうなものが残念ながら必要になる。
大切なのは「自分以外の人は別のプライオリティを持っている」ということを認識し、それを持った上で立ち止まらず進み続けることかなと思う。他人が別のプライオリティを持っているということを知ると、他人がどんなプライオリティを持っているかという点を考慮しながら人間力・政治力を振るうために役立つし、人間力を発揮しなくても、他人の意見は他人の意見として過度に傷つかずに無視して我を通すか諦めるかして次に進むことができそう。
個人的には、既に動いている機能に手を加えるようなアグレッシブな変更よりも、質問の時に弾さんが言っていたように sub じゃなくて fun を作ってみるという手もありだったのになぁと思う(予約語が増えて、既に fun を使っているようなコードにダメージがあるかもしれないが)。有力そうな Subroutine Signatures の実現方法のひとつが序盤でバッサリと切られていたというのは残念。
HASH COLOR
ちょっとしたHTMLはGitHub Gistに置いてbl.ocks.orgで表示するのがお手軽です - Qiita で bl.ocks.org を知り、何か試してみたくなって、入力に応じて色を変えまくるやつ作った。ずっと入力してると気分悪くなる。
http://bl.ocks.org/jewel12/f20ed3003e57cf558e2e
bl.ocks.org は gist の HTML を表示するだけというシンプルさが最高だと思う。
SlackのCUI
https://github.com/jewel12/slacui
チャンネル一覧とチャンネルを指定して読むことしかできない。 percol / peco でチャンネルを絞り込むと少しは便利に使えるけど、毎回API叩くから遅くて使いものにならない。
lacui channels | peco | cut -f1 | xargs slacui read