トップ 追記

日々の流転


2016-01-02 [長年日記]

λ. 2016年の目標

2015年の振り返りを踏まえて、2016年の目標を幾つか。

  • SMT-COMP 参加
  • MOOCの受講 x3
  • 発表 x2
  • 勉強会やイベント参加頻度を増やす
  • プログラミングコンテストとかセキュリティとかはまあボチボチと
  • 語学はコツコツと
  • どっか海外旅行
  • ランニング 400km
  • フルマラソン

2015-12-31 [長年日記]

λ. 2015年振り返り

2015年を振り返ると、色々と翻弄された年だったな、というのが正直なところ。 だけれども、こうして振り返ってみると、それでも割と色々とやっていて、捨てたものでもないかもという気にもなってくる。

お仕事

お仕事的には、某プロジェクトの打ち切りから始まり、その後色々なプロジェクトに参加したりしたけれど、色々となかなか思うように進められず、また色々と思い悩むことも多かった1年だった。 発表としてはコンピュータソフトウェア誌への「SAT問題と他の制約問題との相互発展」の掲載(G+の投稿)と、FIT 2015 (第14回情報科学技術フォーラム) での「地域活性化のためのスマートフォンアプリを用いた実店舗および商品の推薦 」という簡単な発表。 その他には例年通り ICSE 2015 勉強会 で論文紹介をしたりとか。 あと、海外の顧客に対して技術のプレゼンテーションしたりとか、ちょっと面白い経験もできた。

英語とか海外とか

今年は RarejobiKnow もほとんど出来ず。 せっかくおカネを払ってるのだからもっとやらないと勿体ないのだけれど…… ただ、久しぶりに受けたTOEIC(IP)では905点をとれ、前回2008年の885点からは上がってたので、多少なりとも進んでいるのが実感できたのは良かった。

それから、フランスに行ってメドックへのワインを飲んできたり、サルラを観光したりと、遊んできた。 鉄道のストとか、おみやげのフォアグラを空港で急遽消費したりと色々あったが、いい経験と思い出になった。 海外にはずっと苦手意識があったけれど、ようやく慣れてきたかも。

Coursera / MOOC

今年も前半幾つかコースを取れたけれど、後半はそれどころではなかった感じ。

最初に受けたのは Gamificationのコース。 あまり受けたことのないタイプのものだったので、面白かったが、得られた知識はまだあまり活用できてはおらず。

それから、昨年、受講したけど途中で断念した Discrete Optimization を再受講して、最後はギリギリだったけれど、なんとか修了証をゲットするまでできた。 列生成法(Column Generation)とか分枝価格法(Branch and Price)とか気になっていたのが理解できたのは良かった。 以前に受講した Linear and Discrete Optimization と合わせて、これで私も一応は最適化の専門家を名乗っても良いだろうか(^^ まあ、実際には非線形の連続凸最適化とか、カバーできていない領域はまだ色々とあるけれど。

その続きとして、Modeling Discrete Optimization受講したかったけれど、忙しくなってしまってこっちは結局断念してしまった。

もう一つは、Process Mining: Data science in Action の受講で、こっちはペトリネットやワークフローといった比較的馴染み深い話と、データ分析、エンドトゥエンドでのプロセス改善みたいな話がつながってきて、なかなか面白い領域だった。

あと、Coursera’s Global Translator Community (GTC) は参加はしてみたけれど、結局ちょっと翻訳してみただけで、その後の活動が続かなかった。

プログラミングコンテスト系

今年も Google Code Jam はラウンド1を突破できず残念。 また、 ICFP Programming Contest 2015 の方 は結局上位位にはいけなかったけど、色々新しいことを試せたのは良かった。 せっかく最近機械学習とか勉強しているのにDQNを試せなかったのは心残りではあるけれど。

それから、今年も toysolver / toysat を Max-SAT Evalution や Pseudo Boolean Evaluation には出したけれど、アルゴリズム的な改良も特には出来ていたわけでもなく、これも結果は振るわず。一方で、新しいチャレンジとして、MINLPLIB2を変換したものでしかないけれど、問題を投稿するということができたのは良かったと思う。

あと、Proof Summit 2015「SAT/SMTソルバの仕組み」というトークをして、それをキッカケに放置気味だった*1実装を再開して、簡単なSMTソルバの実装ができたのは進捗っぽい。 まだ、SMT-LIB2の仕様を満たせていないのでリリースしていないけれど、満たせたらリリースしたい*2。そして、来年はSMTソルバのコンペであるSMT-COMPに参加してみたいねぇ。 もっとも現段階では本当に最小限の動作をするだけで、性能を云々するところまでいけていないし、これから頑張っても、第一線のソルバと性能を競うところまでは行けそうにないけれど。

それから、以前から気になっていたセキュリティの技術を競うCTF(Capture the Flags)に参加してみれたのは良かった。 CTF for ビギナーズ 2015 東京 に参加して 103人中6位になった後も、Trend Micro CTF Asia Pacific & Japan 2015 Online QualifierSECCON 2015 Online CTF にチームで参加し、それぞれ881チーム中46位と、1251位中43位という成績に。 セキュリティ方面の問題には専門家が多かったので、餅は餅屋ということでお任せして、自分は割とプログラミング系の問題を解いていただけだけれど、後からセキュリティ系の問題も復習したりして結構勉強になった。

コミュニティとか技術トレンドとか

ここ数年引きこもり気味で技術的なトレンドとかをあまり追えていなかったけれど、Proof Summit 2015Haskellもくもく会Tokyo Haskell Meetup に参加して他の人と交流したりと、少しはリハビリできたかな。

新しい言語としては、Goを触ってみたけれど、結局ちょっと試しただけで、それ以上使っていけなかったのは残念な感じ。

余談としては、「flatten=平滑化」事件 とか。

ランニング

3/8の「かつしかふれあいRUNフェスタ」でハーフマラソンの2回目を走った。 その後、今度は今年中にはフルマラソンを一回と思っていたけれど、以前に靭帯を痛めた方の膝の調子が一時期イマイチだったこともあって、結局割とマイペースに走っていた。 年末の恒例の皇居ランではちゃんと2周10km走れて良かった。 合計回数と距離は、Nike+によると今年は104回のランで338.89kmほど走っていたようだ。来年こそはフルマラソンに挑戦したいねぇ。

Ingress

Ingressは 啓示の夜のパワーキューブを観に第18回文化庁メディア芸術祭の受賞作品展示に行ったり、#‎IngressYokosuka‬ のミッションデイ に参加 した以外は、特にイベントにも参加せず、まったりやっていた感じ。 一応レベル15にはなった

*1 SATの実装はあったし、単体法や合同閉包など理論ソルバの実装もあったのだけど、それを組み合わせてSMTとして動かす部分を放置していた

*2 本当はクリスマスにリリースしたかったが……


2015-07-04 [長年日記]

λ. CTF for ビギナーズ 2015 東京 に参加してきた。

CTF for ビギナーズ 2015 東京 に参加してきた。事前配布された資料を読んで比較的簡単そうという印象だったけれど、実際に講義で手を動かしてみたら良く身につきそうで、想像以上に良かった。

最後のCTF実践には「↻」という名前で参加。 16問中13問を解いて、4600点中3200点で、103人中6位だった。実際にCTFに参加するのもとても面白く、はまってしまう人が多いのも理解できた。講義で扱った範囲だけで楽しめる問題をこれだけ作るのは大変だったのではないかと思うし、運営の人たちには本当に感謝したい。

CTF問題メモ

以下、問題のメモを、解き方を忘れないうちに書いておく。 落ち着いて考えれば全問解けたのではないかと思うと、ちょっと悔しいが、初心者なのでまあ仕方ない。

問題1. 練習問題(まずはここから)(最初にこれを開く)(これを解いてから他の問題をやる) (その他 100)

フラグをsubmitする手順の練習問題。

問題2. Can you login as admin? (Web 100)

ユーザ名とファイル名を指定してログインするシステムで、SQLインジェクションを使ってadminでログインする。 講義でやったとおり「' OR 1=1; --」みたいなのを入れたら通った。

問題3. Find the flag (Web 200)

「Flag is hidden in HTTP traffic.」とあって、HTTPヘッダにフラグが書いてあったのだと思うけれど、詳細は忘れた。

問題4. 1M4G3 V13W3R (Web 300)

画像のアップローダが与えられていて、アップロードされた画像は「view.php?file=076b74f36eee552c.jpg」などのようなURLで参照されていた。 「view.php?file=ファイル名」中のファイル名を適当に書き換えると、どうも「images/ファイル名」からファイルを読んでいるようだったので、「view.php?file=../view.php」と「view.php?file=../index.php」でスクリプトをゲット、スクリプト中のコメントにフラグが書いてあった。

問題5. SQL Injection Level2 (Web 400)

SQLインジェクションの2問目。今度はユーザ名は適切にエスケープされていて、パスワード中にORは使えないそうな。 SQLには不慣れなので、SQLを想像して攻撃するのだと自分には難しいだろうなぁ、と思っていたけれど,適当な文字列をいれてログインを試したところ、実行されたSQLがヒントとして表示され、これなら何とかなるかなと思って考えてみる。

どうも「SELECT username FROM users WHERE username = 'ユーザ名' AND password = 'パスワード';」というようなSQLが実行されているようだったので、これは講義中にやったUNIONのやつだと思って試行錯誤。 不慣れなので何回か試したけれど、最終的にはパスワードに「' UNION SELECT 'admin'; --」的なやつを入れていけた。

後で解説を聞くと、ORは一回だけしか消去していなかったそうで、「OORR」とかしても良かったらしい。 しかし、よくよく考えてみると、パスワードにORという文字列が含まれてはいけないサイトって、サイトとしての根本的な機能に問題がある気が……

問題6. Universal Web Page(笑) (Web 500)

「?lang=en」で英語版、「?lang=ja」で日本語版が表示されるようなサイトが与えられていて、フラグはindex.phpに書かれているそうな。「en」や「ja」の部分を書き換えてみると、その名前のファイルをincludeしているらしいので、「?lang=index.php」としてみたが、どうもphpプログラムの実行エラーになってしまってファイルの中身自体は表示されず。 きっとPHPの変態的な機能を使うと、いけると思ったのだけれど、調べてもよく分からず、行き詰まった。

あとで解説を聞くと、「php://filter/convert.base64-encode/resource=」というのを使えばよかったらしく、事前講習資料ではこの機能についても説明されていたようだ。うぐぐ。 しかし、PHPは一体何を考えてincludeにこんな機能を用意しているのやら。 あと、CTFのために、そうでなければ(自分は)学ばないであろうPHPをあえて、しかもこんなマイナー機能を学ぶのもなぁ、という辺りでちょっとモヤモヤする。

問題7. Insecure Protocol (Network 100)

pcapファイルが与えられているので、Wiresharkで開くとTELNETだったのでFollow TCP Streamすると、パスワードがフラグになっていた。

問題8. Insecure Protocol 2 (Network 200)

pcapファイルが与えられており、Wiresharkで開くとTELNETで、こっちはログイン後にフラグが表示されている感じだけれど、肝心のフラグ部分がマスクされている。 対象のホストにtelnetで繋いでpcapファイル中のユーザ名とパスワードでログインするとフラグが表示された。 なんか、telnetコマンドの使い方でちょっとハマった。

問題9. File Transfer Protocol (Network 300)

pcapファイルが与えられており、Wiresharkで開くとftpの通信らしい。ファイルの一覧を表示後、1.txt, 2.zip, 3.txt というファイルをダウンロードしているようだったので、ftp-data でフィルタリングした後に、Export Select Packet Bytes で適当にファイルとして保存し、書かれていてた内容を連結してフラグをゲット。

問題10. This quiz is a NETWORK challenge (Network 400)

今度はpcapファイルではなくexeファイルが与えられている。 実行してみると謎のメッセージが表示される。 ネットワーク問題なので、どうせWiresharkで通信をキャプチャするんだろう、と思ってキャプチャしてみると、Basic認証付きで表示メッセージのデータを取得した後に、Basic認証無しでflag.txtにアクセスしようとして失敗していた。 なので、最初のBasic認証のデータを(base64デコードした上で)使って、ブラウザからflag.txtにアクセスしたらフラグが読めた。

問題11. Communication (Network 500)

pcapファイルが与えられていて、Wiresharkで開くとHTTPっぽかったので、 File → Export Objects → HTTP したところ、lime240.exe (LimeChat?)、rfc1459.txt (IRCのRFC)、trafficというファイルをダウンロードしていていた。trafficを保存するとこれはzipファイルになっていて、中からtraffic.pcapが出てきた。これをWiresharkで見てみるとIRCの通信っぽい。中に「ctf4b{ }」という文字列があるのは発見したが、この個数分の空白をとりあえずsubmitしても不正解、というところで時間切れ。

lime240.exeを保存した上で、それを使って traffic.pcap の中身に従って、IRCサーバに接続して同じことをしてみれば、マスクされていないフラグが表示されたのかな……多分。

問題12. NOT onion (Binary 100)

exeファイルが与えられていて、fileでgifファイルとわかったので、gifとして開いたらフラグが表示された。 画像ファイルからフラグを書き写すのが一番面倒くさい部分だった。

問題13. 読めますか?(Binary 200)

なんか表示できない変なpngファイルが与えられたので、とりあえずstringsしてctf4bでgrepしたらフラグをゲット。 pngとして表示できなかったのは、無理やりファイルを書きかえてpngとして不正なファイルになっていたためか?

問題15. READ and BURST (Binary 300)

アセンブリの実行結果を問う問題。 計算すれば良い。

問題16. DETECTIVE IDA (Binary 400)

謎のファイルが与えられていて、fileコマンドで判別するとexeファイルで、実行すると Passphrase を問われる。 IDA Pro 上で実行して Set IP で Passpharase の判定結果の分岐を正しい方に変更してみるも、文字化けした結果しか出力されず。 多分、パスフレーズのデータも使って復号化する形になっているのだろうと思い、IDA Pro の画面上のディスアセンブル結果でもパスフレーズっぽい文字列が表示されているのも見つけたが、IDA Pro の使い方がよくわからず、色々やっているうちに時間切れ。 後で解説を聞くと、文字列を照合する際の長さとかに注意して、ちゃんと追えばよかったらしい。

問題17. 5394 (Binary 500)

アセンブリの実行結果を問う問題その2。 ループを含む処理になっていて、手で考えるのが面倒臭かったので、とりあえずRubyに書き換えて実行し、フラグをゲット。

問題14?

あと、問題リストをよく見たら、14番めの問題が欠番になっていたことに気づいた。 ひょっとしてURLを書き換えてアクセスすると、隠し問題があったりしたんだろうか?

関連リンク

Tags: security

2014-04-30 [長年日記]

λ. IOモナドでヒープ割り当てを強制される件

Haskellでプログラムを書いていて、数年以上ずっと悩んでいる点として、

sumI :: UArray Int Int -> Int -> Int -> Int -> Int
sumI a i end ret
  | i <= end  = sumI a (i+1) end (ret + (a ! i))
  | otherwise = ret

みたいな関数だと、UArray Int Int -> Int# -> Int# -> Int# -> Int# という型のワーカ関数が生成されるので、結果を即消費するような場合にはヒープ割り当てが発生しないのに対して、

sumM :: IOUArray Int Int -> Int -> Int -> Int -> IO Int
sumM a i end !ret
  | i <= end = do
      x <- readArray a i
      sumM a (i+1) end (ret+x)
  | otherwise =
      return ret

みたいな関数だと、IOUArray Int Int -> Int# -> Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int# #) という型のワーカ関数ではなく、IOUArray Int Int -> Int# -> Int# -> Int# -> State# RealWorld -> (# State# RealWorld, Int #) という型のワーカーしか生成されず、Intが必ずヒープ割り当てされてしまう。

通常は大して問題にならないのだけど、凄まじい回数呼ばれる関数だと、それが積もり積もってプログラム全体のメモリ割り当ての数割を占めてしまったりして、そういう場合にはGCプレッシャーも馬鹿にならないので、出来ることなら1バイトたりともヒープ割り当てしたくないのである。 望む worker-wrapper transformation 結果を手で書いてしまえば良いのだけれど、GHC拡張に依存したコードを直書きするのも気が引けることもあって……

Tags: haskell
本日のツッコミ(全2件) [ツッコミを入れる]

ψ mkotha [ご存知かもしれませんがJoachim Breitnerさんがこの問題に取り組んでますね https://ghc.ha..]

ψ さかい [おお。知らなかったです。ありがとうございます!]


2013-12-31 [長年日記]

λ. 2013年振り返り

2014年を迎えるにあたって、2013年を簡単に振り返ってみる。

月毎の主なイベント

1月
Coursera での学習を開始。昨年末に買ったNexus7で初めてのAndroid経験&初代iPadから乗り換え。
2月
スキーで転けて靭帯損傷。
3月
『型システム入門 プログラミング言語と型の理論』出版と出版記念トークイベントMax-SAT Evaluation 2013 に参加。
4月
特になし
5月
Haskellで計算機代数勉強会を開催。Google Code Jam 2013 は去年に引き続いて今年も体調的に微妙で微妙。
6月
某自社の株主総会見てきた。
7月
スカイツリー昇った。ICSE'13勉強会でT芝チームとして発表。 奥歯抜歯Coursera MeetUp Tokyo に参加。
8月
ICFP Contest 2013 に例によって Team Sampou で参加。引越しと一人暮らし開始。SPLC2013の併設ワークショップFMSPLE 2013で発表。
9月
ウサギと同居開始。
10月
結婚(といっても婚姻届を出しただけで、結婚式はまだ)
11月
電機連合第34回技術者フォーラムに参加。2013川崎国際多摩川マラソンに参加。
12月
川崎グランシティモール実証実験開始

Coursera

前から少し気になっていたCourseraを1月に試してみて、最終的に以下の9コースを履修。

  1. Computing for Data Analysis by Roger D. Peng @ Johns Hopkins University
  2. Data Analysis by Jeff Leek @ Johns Hopkins University
  3. Linear and Discrete Optimization by Friedrich Eisenbrand @ École Polytechnique Fédérale de Lausanne
  4. Machine Learning by Andrew Ng @ Stanford University
  5. Developing Innovative Ideas for New Companies: The First Step in Entrepreneurship by James V. Green @ University of Maryland, College Park
  6. Model Thinking by Scott E. Page @ University of Michigan
  7. Maps and the Geospatial Revolution by Anthony C. Robinson @ The Pennsylvania State University
  8. Introduction to Computational Finance and Financial Econometrics by Eric Zivot @ University of Washington
  9. Introduction to Recommender Systems by Joseph A Konstan and Michael D Ekstrand @ University of Minnesota

自分のスキルのポートフォリオに追加したいと考えたものを中心に、それなりに戦略的に学習してみたつもり。上手くいった部分もあればそうでない部分もあるけれど。自分はデータ分析や統計に関しては大学1年のときに、ほぼ必修の位置づけだった「データ分析」の授業を途中で飽きて切ってしまってから、ほとんど学習しないままになってしまっていたので、その辺りを補完できたのは良かった。

そして、7月にCoursera MeetUp Tokyoに参加したところ、その縁で、メディアで取り上げらることになったのは、なかなか貴重な体験だった。

ルポ MOOC革命――無料オンライン授業の衝撃(金成 隆一)

新しいプログラミング言語、環境

「毎年少なくとも一つの言語を学習する」という話があるけれど、今年は Coursera のコースで割と色々な言語を学べた。 Computing for Data AnalysisData AnalysisIntroduction to Recommender Systems では R を、Linear and Discrete Optimization ではPython (とSymPy)を、Machine Learningでは MATLAB/Octave に触れることができた。その後、そのうちのRとPythonは仕事でもそれなりに使うようになったので、結構役立っている。

それから、言語というほどではないけれど、Model Thinking では NetLogo に、Maps and the Geospatial Revolution では ArcGIS Online に触った。 あと、Introduction to Recommender Systems で使った LensKit は、アノテーションなどを活用したJavaの今風なDIを使ってて、ちょっとおぉと思ったりなんかもした。

『型システム入門 プログラミング言語と型の理論』出版

Benjamin C. Pierce の Types and Programming Languages (TAPL) の訳書『型システム入門 プログラミング言語と型の理論』を出版。前回のAlloy本こと『抽象によるソフトウェア設計−Alloyではじめる形式手法』が終わり、2011年9月からTAPL翻訳が本格始動したのだけれど、それから1年半ほどかかって、ついに出版にこぎ着いたのがこの3月で、非常に感慨深かった。また、共訳者、監訳者、編集者、レビュワー、皆素晴らしい人達ばかりで一緒に仕事をできて光栄だった。出版記念トークイベントという珍しい体験もしてしまったし。

型システム入門 −プログラミング言語と型の理論−(Benjamin C. Pierce/住井 英二郎/遠藤 侑介/酒井 政裕/今井 敬吾/黒木 裕介/今井 宜洋/才川 隆文/今井 健男) Types and Programming Languages(Benjamin C. Pierce)

靭帯損傷

2月にスキーで転けて靭帯損傷。内側側副靭帯損傷の2度で、MRIを初体験したり、しばらくギプス(正確にはギプスシーネ)と松葉杖で不便な生活をしたり、さらに結構な間リハビリをしたりとか。 ギブスしてると、立ってても座っててもバランスが悪くて、体中凝って仕方なかったのが辛かった。 後、しばらくギプスとサポーターをしてるだけで、関節って本当に曲がらなくなるんだなぁ。リハビリしてだんだん動くようになって、人間の関節や筋肉って本当によくできてるなぁと思った。 大変な体験だったけれど、周囲からは非常によくしてくれたし、結構学ぶことのあった体験だったと思う。

ランニング

ランニングは500kmの目標を立てていたけど、途中怪我で数ヶ月走れなかったこともあって、320kmほどに留まった。でも、我ながらよく続いたなぁと思うし、自分を誉めてあげたい。 また、大会に参加するという目標は2013川崎国際多摩川マラソンに参加するという形で達成。 目標がハーフマラソンだったのに対して8kmになってしまったので、ハーフマラソンを走るのは2014年の目標に持ち越し。

あと、昨年末にちゃんとしたランニングシューズを買ったけれど、今年は心拍計 Wahoo Blue HR とか、活動量計 Misfit Shine とか、ランニング用のスポーツタイツのCW-Xとか色々と買ってしまった。

お仕事

Courseraで学んだデータ分析・機械学習系の知識を活かして、これまでとちょっと違った方面の仕事に挑戦してみた1年で、川崎グランシティモール実証実験 なんかにも関われて、まだまだこれからだけれど、面白い仕事ができた。

その他にはFMSPLEで発表したりとか。

計算機代数

代数的実数や量化子除去に関して勉強したり簡単な実装をしたりしていたので、思いきって Haskellで計算機代数勉強会という勉強会をゴールデンウィークに開催。結構マニアックなトピックにも関わらず参加者20人以上も集まり、なかなか楽しかった。 その後も、Berlekamp-Zassenhaus アルゴリズムを理解して実装したりとちょっとは進めた。あと、これまでなんとなくしか理解できていなかった sugar flavor とか syzygy とかについて、計算機代数勉強会での@mr_konnさんの発表で理解できて、自分でも実装してみようと思っていたけれど、これは実装しないままになってしまったなぁ……

Max-SAT Evaluation 2013

昨年は Pseudo Boolean Competition 2012 に参加したが、今年は開催されなかったので、代わりに Max-SAT Evaluation 2013 に参加。 今回は自分のtoysatに加えて、GLPKSCIP に簡単なフロントエンドを付けたもので参加。

自作のtoysatの方は、昨年の Pseudo-Boolean Competition 2012 ではそれなりに健闘した(と思ってる)けれど、今回はあまり振るわなかったねぇ。 まあ、色々とやりたいことはあったけれど、結局、目的関数値の線形探索ベースの単純なアルゴリズムのやつで投稿してしまったからなぁ……

SCIPの方は、SCIP本体のバグが見つかって、SCIP開発者に報告・修正してもらったものを再投稿させてもらったりと、意外と大変だったけれど、その甲斐もあって Partial Max-SAT 部門の Crafted ベンチマークで2位に入賞して嬉しかった。(別にフロントエンドを書いただけの自分がすごい訳ではないのだけれど)

英語

英語は今年はあんまり頑張れなかった。 Courseraでは英語を使って学習してはいたし、日本開催の国際会議SPLC2013の併設ワークショップFMSPLE 2013で発表はしたものの、海外には一回も行かなかったし。それに、レアジョブも後半は殆どやらなくなってしまったしなぁ。2014年はその辺りもっと頑張りたいところ。

関連エントリ