トップ 追記

日々の流転


2017-01-18 [長年日記]

λ. 2016年振り返り

全般的に体調的にも精神的にも低調で、倦怠感にずっと悩まされ、精神的には悩んでも仕方がないことに悩み、理不尽に対して無駄に怒りと鬱憤をため、あまり生産的な方向にエネルギーを使えなかった一年だった気がする。 自分にコントロールできないことには囚われず、コントロールできることに集中すべきなのだけど、そういう割り切りそれ自体を維持するにもエネルギーがいるよね。

年初の目標を振り返ってみると、達成できなかったことも多いけど、かといって全く何もやっていなかったわけでもないことが分かって、ちょっとポジティブな気持ちになった。

  • SMT-COMP 参加
    • → 自作のSMTソルバtoysmtに、有理数線形算術の理論と、非解釈関数(uninterpreted functions)の理論を実装して、SMT-COMPに参加。 出場した全てのカテゴリ(QF_LRA, QF_UF, QF_UFLRA, QF_RDL)で最下位という予想通りの結果だけれど、とりあえずちゃんと動いたようで良かったよかった。 その後、ビットベクタの理論については実装したし、後は整数線形算術の理論に対応したうえで、性能をもう少しなんとかしたいところ。 やりたいことに対して歩みは遅いけれど地味には進められているかな。
  • MOOCの受講 x3
    • → Courseraのガロア理論のコースを受講してみてたけど、途中でついていけなくなって、次の回にスイッチして復帰しようともしてみたが、結局復帰できないままになってしまった。他に、UdacityのTensorFlowでディープラーニングを学ぶというコース も覗いてはみたものの、こちらは本格的に取り組むことはなかった。 年の途中で一回仕切りなおしたかった。
  • 発表 x2
    • Haskell Day 2016 で SAT/SMT solving in Haskell という talk をした(slideshare, PDF)他、小ネタとしては恒例のICSE2016勉強会で論文2本を紹介(PDF)したのと、某イベントでMOOCについて簡単に紹介した(slidehare, PDF)くらいか。 お仕事での発表が全くできていないのが残念……
  • 勉強会やイベント参加頻度を増やす
    • → 機械学習・データ分析系の勉強会には何度か参加して、勉強にはなったし、空気が分かったのは良かったけれど、ただネットワーキングという意味ではあまり広げられなかった感じ。あと、某社内コミュニティ(参考)に参加してみたのは良かった。 Haskellもくもく会はちょっと参加したけれど、もっと出たかった。
    • → イベントに関しては奈良で開催されたICFP 2016、千葉で開催されたATVA2016に参加できたのは良かった。
  • プログラミングコンテストとかセキュリティとかはまあボチボチと
    • → CTFについては、DEF CON CTF 2016 Qualifiers (writeup), MNCTF2016 (writeup), Trend Micro CTF 2016 Online (writeup), HITCON CTF 2016 (writeup), SECCON 2016 Online CTF (writeup) と、5回参加できた。 ただ、あんましセキュリティ的な要素のない問題ばかり解いていたので、セキュリティ系のスキルが向上した感じはないけれど。
    • → プログラミングコンテストは、ICFP Programming Contest がせっかくの日本開催の貴重な機会だったので、運営側のチームに混ぜてもらったのだけれど、途中で脱落してしまった。 参加者としては参加せず、運営の様子を裏からちょっと見ていて、それはそれで貴重な機会ではあったけれど、本当に残念なことをした感じ。 他には Google Code Jam とかに参加したくらいで、これもパッとせず。
  • 語学はコツコツと
    • → rarejobは結局年の初めと終わりの数えるほどしかできず。iknowの方はもう少しできたけれど、まああんまりコツコツ続けられた感じはしない。TOEIC(IP)はちょっとだけ上って925に
  • どっか海外旅行
    • → どっかアジアにでも行きたいと思っていたが、結局行けず。
  • ランニング 400km
    • → 距離はトータルで179kmほどで、目標の45%ほどに留まった。 月別では1月19.6km、2月14.3km、3月39.0km、4月9.9km、5月14.9km、6月16.2km、7月8.4km、8月2.5km、9月7.6km、10月2.8km、11月11.1km、12月32.4kmという感じ。 倦怠感に負けた。
  • フルマラソン

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..]

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