SMT Solver無しでXorshift128+を解く

先週のCBCTFではXorshift128+の32個の出力列が与えられた場合にその先を予測させる問題が出題された（Random RSA）。

想定解はSMT Solverを使うのだが、宗教上の理由で使えない人が居るかもしれないため別の解法を考えた。

なお、先に言っておくとこの解法は多大なリソースを必要とし、具体的にはメモリを200GBほど使用する。研究室の500万円の計算機で64Thread立てて計算しても30分ほど掛かった。要するにz3を使え、その辺のパソコンで10秒で解ける。

Xorshift128+とは

while True:
    s1 = s[0]
    s0 = s[1]
    s[0] = s0
    s1 ^= (s1 << 23) & ((1<<64) - 1)
    s[1] = s1 ^ s0 ^ (s1 >> 18) ^ (s0 >> 5)

    yield (s[1] + s0) & ((1<<64) - 1)

Xorshiftとは主にxor, bitshiftで構成された軽量な乱数生成器である。Xorshift系の乱数生成器には様々なバリエーションが有り、その中の1つであるXorshift128+はadditionを加えることで線形性を除いている（後述）。なお、128とは状態数が128bitなことに起因すると思われる（もしかしたら周期かも？）。

Xorshift128+の難しさ

もしこの出題が普通のXorshift128であったなら簡単に解くことが出来る。

何故なら、Xorshift128に使われる処理はxorと固定長bitshiftだけであり、これらは共に状態bitをGF(2)上のベクトルと見なせば線形性を持つ。つまり、全ての演算が行列で書き表せる為に逆行列を作ることで簡単に初期状態を復元できる。

しかし、Xorshift128+の出力列は最後に加算される。この処理は線形性を持たない。この簡単な処理を付け加えるだけで問題は飛躍的に難しくなる。

Xorshift128+の線形性

しかし、Xorshift128+であっても線形性を持つ箇所がある。LSB（最下位bit）である。

LSBは下の桁が無いため、繰り上がりを気にしなくても良い。その為32個の出力列から32個の線形方程式を得ることが出来る。もう少し考察すると、注目するbitより下位が全て1である場合も繰り上がりを気にしなくてもよく、N個の出力列からおよそN/2個の方程式を得ることが出来る。

Random RSAでは新たに28個の線形方程式を得て、60個の方程式が集った。

行列に対するMITM

60個の方程式を集めたということは、128bit中60bitがleakしたと考えることが出来る。しかしまだ68bitの総当りが残る。

これを何とかしてMITMで計算量を落とせないか考えた。ここからの説明はかなり雑なので分かる人しか分からないと思う（真面目に行列の式書くのがめんどい……）。

ここから内部状態を64bitずつのx, yと表すことにする。

今60個しか式が集まっていないが、適当に4bit固定することにより64個の線形独立な式を得る。この行列を変形し、[E | M]のように左半分を単位行列とする行列を得る。これにより、xとyの関係を線形方程式で記述出来る（x + My = 64次ベクトル）。

ここで1つ目の出力列により、yを定めればxが定まる。また、先述の線形方程式からもyを定めればxが定まり、これらが一致すれば解となる。

ここでyを上位32bitと下位32bitに分割する（y1, y2）。そうすると先の線形方程式はx + M1y1 + M2y2 = 64次ベクトル という様な式に変形できる（y1, y2を定めるとxはそれぞれ繰り上がりの有無を無視すれば一意に定まることに注意）。以上から、M1'y1 + M2'y2 = 64次ベクトル という式を得る。

これは、M1'y1 - 64次ベクトル とM2'y2をそれぞれ独立に計算し、一致する場合を探せば良い。

これを実装すると64個の解が出てきた。これは最初に足りない4bitを定めた分と無視した繰り上がりの2bitで6bitの自由度を持った為だと考えられる。あとは全て試すと正しい解を得た。

enumulating all y1
merging vectors
miv1: 8589934592
enumulating all y2
merging vectors
miv2: 4294967296
serching
2476520362 61509141
2157264084 3353016742
656009753 1860619162
2574392452 2567461328
3446121306 463614785
3288533184 2667169677
3065249141 186478286
769889559 1500841788
540840065 3086893980
1799405833 2135579198
954749789 548963819
3960811688 2581296186
3103250995 4048812002
2904438575 287535986
1008273453 742342059
1609709208 525912563
102537622 2128507249
2446164013 1093192679
2075536625 1789293171
1195834711 2725839867
295618493 3554538105
2373988069 3548126869
1347207931 483994859
1071373495 101210017
193547184 2191692163
1021151311 519290032
1916084563 544594116
2047105320 318595631
66506444 2834209036
1251206337 3094191279
4186820173 2782881948
2114031298 3190589275
508037032 453555974
745063296 2750048806
2923802844 1177402636
2832440853 273566763
1518323354 358834199
1122617837 2403936068
1091218555 4018685749
4136247442 294350163
2928405395 1799492342
2197082799 759383716
4077570164 1016706399
3093126019 3118276782
2943083703 1649561999
3404147677 124557829
716115770 275919643
2901710221 4203208796
657711912 331906217
2690332004 2083220237
433830677 896965898
1296534180 1664930400
1977485902 3742108858
3115534102 689202550
1477097847 3976949959
378126705 2382484743
2943110840 288054401
3860062577 4057827336
1338808793 100592408
133487806 3607172407
2616266322 477564116
3764152924 916057340
1307750470 153169944
1629761026 657825298
829409657 396404147
3151417975 3300223157
2494409012 3774521208
3045576677 1401251776
1775617714 3515828845

y1, y2 = 508037032, 453555974が答え。

実装

64Threadで実行して30分くらいだった。

GF(2)上であれば行列積がandとbitcountになることを使って高速化したりしたがまだまだ重い。ソート列のマージをシングルスレッドで行っているのがボトルネックで、頑張れば10分を切るくらいにはなると思う。メモリも工夫すれば60GB程度には減らせそう。最初はy2の列だけ生成して各y1で二分探索していたのだけど期待よりかなり重くなった。研究室マシンが1.5TBのメモリを持っていたので雑に両方持ってやったほうが速いようだ。

あと普段競プロで並列化やメモリキャッシュやらに気を配ることが殆ど無いのでこのあたりのノウハウが皆無なことに気がついた。悲しい。

GitHub - aki33524/xorshiftplus

CBCTF Writeups

miyaji-labで参加した。これは暗号系研究室に所属している以上Cryptoを全完するという強い決意を表している（大嘘）。

結果としてはRandom RSAを時間中に解くことが出来なかった。悲しい。

 

Common Modulus 1

  Common Modulus Attackをする。

Common Modulus 2

Common Modulus Attack 1と異なりeが3を最大公約数として持つので、m3 mod nが求まる。

mが十分に小さいのでm3 % n = m3となり、二分探索により3乗根を解けば良い。

Common Modulus 3

平文mの後ろに0をpaddingするということが左にbitshiftする(_m * = m * 2x)ということに気がつけば簡単。

これまでと同様にm17 mod nを得るが、m17 = (m * 2x)17 = m17 * 217*xとなる。

xはこれまでのフラグから適当に定めて217*xの逆元を掛けてやるとm17 mod nを得る。

Common Modulus Attack 2と同様の考察から17乗根を求めると良い。

Pailler Oracle

Pailler暗号に対する選択暗号文攻撃をする。得られる情報は復号した結果のLSBである。

Pailler暗号は加法準同型を満たす珍しい暗号である。

また、Pailler暗号は加法準同型だけで無く、mに対する暗号文cが得られている時、任意のrを選択しm*rの暗号文c'rを作成することが出来る。

これら2つの性質は今回の問題において平文に対する加減乗除が行えることを示唆する。

よってm-1とm/2の演算を行うことにより、mを右shiftした平文に対する暗号文を作成することが出来る。

つまり、LSBが0のときはm/2をし、1のときは(m-1)/2をする。これを繰り返すことで全てのbitをleakすることが出来る。

余談

準同型性でLSBの情報がleakすると言えばRSAのBleichenbacher Attackの亜種が有名である。実はこの知識があったせいで変に勘ぐりすぎて時間が掛かった。

詳細は割愛するが、nが常に奇数なことによりLSBからmの範囲を限定する（上位1bitをleakする）。これを繰り返して二分探索のようにすることでmの全体を得る。

同じような攻撃が成り立つのだろうとしばらく複雑に考えてしまったが、Pailler暗号は加法準同型を満たすことを冷静に考えたら解けた。

ちなみに僕はまだPailler暗号が何故成立するのかを理解しておらず、式を眺めれば解けた。この理解の放棄は上手く行ったと思う。

あと、netcatで上手く整数を取得する方法が分からなくてかなり汚いコードになった。良いやり方を知ってる人は教えてください。

Smoke on the water

eが大きいと言えばWiener's attackというのが相場である。これはeが大きいことが本質ではなく、その時にdが小さくなり得るのが問題である（実際にはほとんどのdが小さくならないので余り気にしなくて良いのではないかと考えている。この点について詳しい人が居れば教えてください）。

実際、式中でd_が小さいことが保証されているのでWiener's attackを使うのがほぼ確定する。

まずコード中の式を変形するとd = (p-1) * (q-1) - dよりe * d = e * ((p-1) * (q-1) - d) = -e * d_ = 1 mod phi(n)である。

普通のWiener's attackはe * d = 1 mod phi(n)においてdが十分小さい時にn, eよりdが求まるというものである。

よって既存の手法のe * d - 1とある箇所をe * d + 1（ここにおけるdはd_なことに注意）と書き直せば良い。

これによって求まる d_を用いてcd_ = m-1 mod nを求め逆元を取ると良い。

余談

Wiener's attackは名前と成立条件だけ知っていて、詳細を知らなかった。そこで既存のコードを変形することを軸に考えたのが上手く行った。問題を開いてから10分も掛からなかったと思う。

Random RSA

この問題は2つのフェイズに分かれる。乱数列を予測するフェイズとそれを元にmを復元するフェイズである。

乱数列予測で沼にハマったが、これはxorshift+と呼ばれるものでz3というSMT solverを用いれば簡単に解けるようだ。

http://inaz2.hatenablog.com/entry/2016/03/07/194034

そこからmを予測するフェイズであるが、これは実は2つの平文があれば解くことが出来る。

ある2つの暗号文c1 = (m + b1)e, c2 = (m + b2)eとb1, b2と公開鍵が得られている時、mを求めることが出来る（Franklin-Reiter related-message attack）。

これは(x + b1)e - c1 = (x + b2)e - c2 = 0において、2つの多項式が共通の多項式(x - m)を持つことを利用して多項式におけるgcdを解く。

ということを普段多変数多項式の研究をしている研究室の友人に言ってみたところMangaで解いてくれた。

余談

実はSMT solverを使わなくても32個の出力列を使えば解けるのではないかと思う。ただかなり実装が面倒な上、もしかしたらSMT solverの再開発かも知れない（SMT solverの中身を知らない）。

Franklin-Reiter related-message attackのことを何も理解していないので理解したい。

所感

久々のCTFの割に解けたほうだと思うが、勉強不足を痛感した。それに加えて下手に知識を得ていたせいで調べることを放棄して無駄に考えてしまう時間が長かった。この辺りはCTF慣れだろうか。

KRACKについての私的まとめ

技術詳細を解説した日本語記事が見当たらなかったため簡単に纏める。

なお、冗長になるため断定調で書いているが怪しい箇所も多い（間違ってたら教えてください）。

あと、図は無いです（許して）。

WPA2とは何か

新しい規格である802.11iの標準化が進められていた当時、WEPが破られた。そのため11iを部分的に実装したものがWPAである。その後、AESや1xに対応した11iに完全に準拠した実装が作られた。これがWPA2である。

WPA/WPA2はMIC（メッセージ認証コード）やreplay counterにより改竄とreplay attackを防いでいるのもWEPとの大きな違いである。

WPA2の仕組み

WPA2の接続認証には2つの方法がある。PreShared Key（事前鍵共有）と1xである。前者は小規模の環境で使われる同じパスワードを使う認証であり、後者は大学など大きな環境で使われる（認証サーバーが別途必要）。

ただ、KRACKを理解するにおいて両者の詳細を知る必要は無く、どちらの方法であっても同一のPairwise Master Key（PMK）をAPとClientが持つことさえ分かれば良い。もちろん、PMKは盗聴者に対して秘匿されている。

その後、4-way handshakeにより、PMK, Anonce/Snonce, MAC addressからPairwise Transient Key（PTK)という一時鍵を生成する。PTKを元に5つの鍵を生成する。これらはunicast通信の暗号化（PTK-TK）、後に配布するbrouadcast通信の鍵の暗号化、MICの鍵として使用される。

Msg1: APからAnonceを配布
Msg2: ClientからSnonceを配布

この時点でAPとClientはPTKを生成することが出来る。

なお、ClientはMsg1の時点でPTKを生成することが出来ているため、それを元にMsg2はMICが付加されている。

APはそのMICが合っているかを検証し、Clientが正しくPMKを知っているかの認証が行える。

Msg3: APからGroup Temporary Key（GTK)を配布

これにもMICが付加されている。この時点でClientはPTKをinstallする。

Msg4: ClientからACKを返す

この時点でようやくAPはPTKをinstallする。

PTKのinstallとは何か

セッション中は同一のPTK-TKを用いるのだが、そのセッション内での鍵が同じであった場合、同じキーストリームが生成される。それを避けるため、実際にはInitial Vector（IV)を付加して少し鍵を変える。IVは1パケットごとにインクリメントされ、二度と同じIVとPTK-TKの組み合わせが生じないようにされている。

攻撃の詳細

11iでは、ClientがMsg3を受け取れなかった場合に備えて、再送することになっている。再びMsg3を受け取った時、Clientは鍵をre-installする。この際、IVが初期値に戻ってしまうため、同じIVが使われる事となる。

Msg3を再送してもらうために、攻撃者はChannel-based MitM（APとClientに対するMan-in-the-Middle手法）によりAPとClientの間の通信を妨害する。具体的にはMsg4が届かないようにする。それによりAPはMsg3を再送し、攻撃者はそれをClientに渡すことでre-installが行われる。

前述のようにWPA/WPA2ではreplay attackが出来ないため、この様に面倒な手段を取る必要がある。

あるIVが使われている暗号文の平文が既知である場合、そのIVにおけるkey streamが分かる。それにより、同じIVが使われている全ての暗号文の平文が分かる。

なお、wpa_supplicant2.4ではre-installの際にPTK-TKが0に初期化されてしまう問題が存在した（これは11iがinstallした鍵は0で埋めることを推奨しているため）。

Q&A

WPA-TKIP（RC4）はstream cipherだがWPA-CCMP（AES）は違うのでは

CCMPのAESはCTRモードで、実質stream cipherとして用いられている。しかし、CBC-MACにより改竄が検知されるため、CCMPではinjectionが不可能である。

実際どれくらい攻撃出来るのか

筆者らの実験では、WindowsやMacOSはMsg3の再送を受けてくれず（これは11iの仕様に則っていない）、実質攻撃可能な環境はそれほど多くなかったようだ（Group Key Handshakeに対する攻撃は全ての環境で適用出来ているので、Windowsが当てたパッチはおそらくこれ）。

また、Channel-based MitMは攻撃対象のAPより攻撃者のAPのほうが電波が強い必要があり、つまりは成功率はどれほどターゲットに近いかに依存する。

ICPC2017国内予選

きゅうりが消えたため、たこの友人を新しくチームメイトに加えた。

なお彼は競プロ初心者らしいのだが、頭が良いのでアジア地区では化けてくれると信じている。

僕らのチームはどちらかというと考察が得意で実装が苦手なため、初動で遅れることは予想していた。その為焦らずに正答数を伸ばすことを心がけていた。

結局ペナルティ差で後輩チームに負けてしまったが、阪大で2チーム突破は多分初なのでめでたい。

f:id:aki33524:20170715173602p:plain

A, B, Cはそれぞれが並列で解いてあとは流れでやろうという話をしていた。僕がC。やるだけ。

A, Bがそれぞれちょっと詰まっていたけど当初の目標であった3問1時間以内は達成された（遅すぎる……）。

その後、僕がDを読む。最初はmod 2における行列の一次独立とかrankとかそういう話なのかなぁと思いそれにハマってしまった。行列計算はちょうどO(NM)が出現するのでそれもハマりの補助となった。 DPと全探索はすぐに見えていたので、冷静に計算量を書いたら分かった。去年の筑波のI問題を彷彿とさせる問題だと思う。考察に時間がかかり過ぎた上にDPフェイズで結構バグらせた。この程度は一発で通せるようになりたい。

たこらがEを読む。最小積和形にすればいいんじゃないかとかなんとか言っていた気がする。結局文字数の制約に気がついて考察は立った。

とは言えこの時点でまだ4完。残り時間は1時間を切っていた。普通に落ちる未来が見えて焦った。

多分僕はEよりFが得意だろうと判断して考察する。紙で色々書いていると方針が立つ。残り30分。Eはバグったらしい。

Eのバグを取りつつ紙で詰める。indexが厄介なので実際に各操作を手で試してみて両端と真ん中が整合性が取れていたらOK！という経験上バグりにくく且つ高速な方法を取った。

残り15分。僕がFを実装しながらEを紙でデバッグ。Fもバグる。印刷。

残り10分。Eのバグが分かったらしい。書いてもらう。僕もFのバグを見つける。条件やら操作は全て合っていて一箇所typoが合った。これを見つけたのは奇跡だった（経験上typoのバグは焦るとマジで見つからない）。

残り4分。Eが通る。僕に代わる。

typo修正してサンプルが通る。実行して出力を確認せずに投げる（時間がなかったため）。手が震えてコマンドめっちゃtypoしてた。

残り2分。Fが通る。皆でワイワイしていた。

終了後後輩チームらと飯を食べながら解法議論していた。彼らのF問題の解き方はイミフ過ぎたし、彼ら自身も全く証明していないらしい（サンプルが強いためサンプルが通ればまずOKという見立ては非常に正しいと思う）。Gはフローじゃないかなぁということを話してご帰宅。

経験上僕は焦った時のパフォーマンスが著しく落ちるので、Fを実装するときは努めて落ち着くようにした。結果かなり良いパフォーマンスが出せたと思う。良い経験ではあったが、二度とやりたくない。

WoTの当たり判定を色付きで表示するMODを作った

github.com

動機

最近World of Tanksという戦車ゲームにハマった。嬉しいことにこのゲームはMODを作ることを歓迎している。

戦車の装甲値などを一覧で見たかったので、csvにまとめるツールを作った。

github.com

しかし、実際には戦車の装甲値は位置によって異なる。これを文字だけで認識するのには限界がある。そこで戦闘中に3Dモデルとして表示することにした。

先駆者

WoTで当たり判定を表示するのにはいくつかの先人がいる。

Web上で見られるものではtanks.ggが有名。

World of Tanks - tanks.gg

MODとしては、PROTankiがガレージで表示するものを作成している。他にも幾つかあるようだ。

しかし、確認した範囲ではこれらは戦闘中の表示には対応していないようだった。また、モデルを改竄（以下model hack）しているのではなく、コードを改竄（以下code hack）しているらしい。

それに対して、code hackではなくmodel hackだけで実現しようと考えた。理由は下記。

  1. code hackではバグにより意図せずチートを入れ込んでしまうかもしれない
  2. code hackではデバッグが大変そう（ほんまか？）
  3. 表示のことは表示（model）で担いたい

技術詳細

簡単にやったことを説明する。

各戦車はitem_defs/vehicles以下の定義ファイルによってモデルが定義される。

戦車のモデルとは大きく4つのモデルから成る。車体、砲塔、砲身、履帯である。

また、それぞれのモデルは見えるモデル（以下normal model）とは別に、当たり判定モデル（以下collision model）を持っている。 厳密はクライアントで取得できるcollision modelはcollision_client以下に入っており、サーバーサイドのものとは異なるようである。ただ、大差無いだろうということでクライアントのものを使う（というかそれしかモデルを取得できない）。

アイデアとしてはnormal modelをcollision modelに変えるだけである。

各modelは3つのファイルからなる。.model、.visual_processed、.primitives_processedである。

.model

各戦車の定義ファイルから参照される。Level Of Detailを管理する。

.primitives_processed

モデルの頂点群、ポリゴン、ノードを定義する。

.visual_processed

ポリゴンとテクスチャの結びつけ、シェーダーを管理する。

では、normal modelの.primitives_processedと.visual_processedをcollision modelに差し替えれば動くだろうか。

実際このアイデアだけで車体と砲塔は問題ない。また、装甲値は定義ファイルに入っているので、それによって.visual_processed内のテクスチャの参照を書き換えるだけでいい。

しかし、砲身と履帯はもう少し厄介になる。

車体と砲塔、砲身と履帯の違いは「動く」かどうかである。砲身は撃った後のリコイル処理、履帯は言わずもがなである。

当たり判定は動かないモデルであるから、車体と砲塔のように動かないモデルと差し替えるのは比較的簡単であるのだが、砲身と履帯はもう少し工夫が必要となる。

ここからはスキンメッシュアニメーションの理解を前提とする。

戦車のモデルはコード中で組み立てられる。.visual_processedや定義ファイル、また通信によって得られた情報を元に動的に構成される（そうでなければ砲塔は回らない）。

砲身と履帯にはボーンが定義されていて、コード中でそのノードを参照する。つまり安易にモデルを差し替えてノードを消してしまうと参照エラーでクライアントがクラッシュする。

比較的簡単な砲身から見ていこう。

.visual_processedの中にはrootの下にGunというnodeが存在していて、それが実際に動く箇所らしい。

そこで、collision modelの.visual_processedの中でrootではなくGunを参照するように書き換えれば良い。

次に履帯。これは非常に苦労した。

履帯は車輪、サスペンション、トラック（回っている部分）からなる。また、車輪の数などは定義ファイル中に書いてあり、それによってコード中で構成される。

しかしこの定義を書き換えると.primitives_processedとの対応が取れずにクラッシュする。しかも、コード中で駆動輪が2つ無いとエラーを吐くようになっているので、model hackだけでは差し替えることが出来ない。

そこで、normal modelとcollision modelの.primitives_processedをmergeした上で、.visual_processedを改竄してnormal modelだけ見えないようにすることを考えた。これならnormal modelは存在しているので参照エラーは起きない。

normal modelを透明にするには幾つかの方法がある。

  1. テクスチャを透明にする
  2. 元の.primitives_processedを改竄してポリゴン数を0にする
  3. ボーンの変換行列を0にする

選択したのは3の方法である。最初に1をやろうとしたのだができなかった。後から気がついたのだが、これはシェーダーも弄ってやる必要があったらしい。2も挑戦したのだが、.primitives_processedの仕様を把握できず断念した。

3はスキンメッシュアニメーションの仕組みを調べている時に思いついた。.visual_processedでは親nodeに対する回転行列とオフセットを持っている。この回転行列を0にすることで自身以下のnodeを1点に集めることが出来る。つまり透明になる。

合法性

このMODを公開する前に日本のスタッフに聞いたところでは合法だった。

blog.livedoor.jp

forum.worldoftanks.eu

小話

何故クライアントはcollision modelを持っているか

当たり判定処理と言うのはサーバーサイドで行うべき処理なので、クライアントに入っていることが疑問だった。

多分答えの一つはシンプルで、地面や建物との当たり判定はクライアントに担わせるべきであるからだ（normal modelはポリゴンが複雑なのでそれと当たり判定を行うのは難しい）。

ResMgr

WoT（というよりBigWorld）で使われている仮想ファイルシステム。

wotmod.mtm-gaming.org

この検索は非常に「柔軟」である。どうやらファイルのindexを構築する際に小文字に変換するのか大文字小文字の差無くマッチする（後から気がついたので対応が面倒だった）。それだけならまだしも、ディレクトリのパスが'/‘でも’\‘でもマッチする。何故か両方が混ざっているファイルパスが存在していた。勘弁してくれ。

戦車訓練でPantherの砲身が消える

何故か戦車訓練のPantherのcollision modelには砲身が存在しない（普通のPantherには存在している）。つまり、戦車訓練ではPantherの砲身にダメージを与えることが出来ないはずである。あの世界では敵が撃ってこないので確かめる術はないが……。

空間装甲を半透明にしたい

collision modelのデフォルトのシェーダーはlightonlyというものである。これをlightonly_alphaやlightonly_addにすることでアルファブレンディングを行ってくれる……はずだった。ガレージではちゃんと半透明に表示されたのだが、戦闘に出ると履帯が丸ごと消える。謎。

GCJ 2017 Round 1B

B問題をクッソバグらせて絶望していたがCが瞬殺されてギリギリ964位だった。初Round1突破っっぽいので記念に解説を書く。

A

略解

一番ゴールするのが遅い馬と同時にゴールする。

証明

一番ゴールするのが遅い馬（以下B）に注目する。

  1. Bと自身（以下A）が同時にゴールするようにした時、AはゴールするまでBに追いつかない。 AとBは共に等速であるから、距離は線形に縮まる。最初正の距離が開いており、ゴールする時に0であるからそれまで追いつかない。

  2. BとA以外の馬（以下まとめてCとする）について、Cは必ずBに追いつく。 順番待ちルールがない場合、CはBより先にゴールする為これは明らか。Bに追いついてからは1よりAはCにも追いつかない。

  3. CがBに追いつくまでに、AはCに追いつかない。 順番待ちルールが無いとすると、CはAより先にゴールする。1と同様の議論からAはCに追いつけない。

以上から、Bのみを考えればCは考察する必要が無い事がわかる。

文字で書くと冗長だが、馬の変位軸と時間軸のx-tグラフを描けば直感的に理解できると思う。

#include <bits/stdc++.h>
using namespace std;

int D, N;
vector<double> K, S;

void solve(){
    double mtime = 0;
    for(int i=0; i<N; i++){
        mtime = max(mtime, (D - K[i]) / S[i]);
    }
    cout << D / mtime << endl;
}

int main(){
    cout.precision(16);
    cout.setf(ios::fixed);
    
    int T; cin >> T;
    for(int i=1; i<=T; i++){
        cout << "Case #" << i << ": ";
        cin >> D >> N;
        K.resize(N);
        S.resize(N);
        
        for(int i=0; i<N; i++)
            cin >> K[i] >> S[i];
        
        solve();
    }
    
    return 0;
}

B

略解
  • small

最も多い色を並べ、残り2色を左右から一つ飛ばしで挿入していく。

  • large

R -= G, Y -= V, B -= Oとしてsmallと同様の問題を解いた後、残った色を挿入。

証明

対称性から、Rを最も数が多い色として一般性を失わない。

  1. R > Y+Bであるなら、IMPOSSIBLEとなる（必要性）。 どのように挿入してもRが隣り合うので自明。

  2. IMPOSSIBLEであるなら、R > Y+Bである（十分性）。 対偶をとって、R <= Y+Bであるなら必ず解を構成できることを示す。 これはRの左右からY, Bをそれぞれ挿入すると良い。

  3. GはR、OはB、VはYとしか隣合えない（題より）。 small解けてlarge解けてない人はこの制約を見逃していそう（僕がそうでした）。

  4. GとRしか存在しない時、G == Rの場合しか解が存在しない（対称性よりO, Vは略）。 GRGR…となるケース以外は明らかに同じ色が隣り合う（鳩ノ巣原理？）

  5. GとR以外にも色が存在する時、R -= Gとして問題を解くことが等価（対称性より(ry）。 Gは（Gを含めて）R以外と隣合えないので、RGR…RGRという風にRで両端をサンドイッチする必要がある。 これは先頭のRGR…RGを取り除いてRのみとして問題を解くのと同じ。

#include <bits/stdc++.h>
using namespace std;

int N;
int R, O, Y, G, B, V;

string solve(){
    string table = "ROYGBV";
    if(R == G && (Y|V|B|O) == 0){
        string res = "";
        for(int i=0; i<R; i++)
            res += "RG";
        return res;
    }
    if(Y == V && (R|G|B|O) == 0){
        string res = "";
        for(int i=0; i<Y; i++)
            res += "YV";
        return res;
    }
    if(B == O && (R|G|Y|V) == 0){
        string res = "";
        for(int i=0; i<B; i++)
            res += "BO";
        return res;
    }
    
    R -= G;
    Y -= V;
    B -= O;
    
    if(R < 0 || Y < 0 || B < 0)
        return "IMPOSSIBLE";
    
    if((R==0 && G!=0) || (Y==0 && V!=0) || (B==0 && O!=0))
        return "IMPOSSIBLE";
    
    if(R>Y+B || Y>R+B || B>R+Y)
        return "IMPOSSIBLE";
    
    bool ymax = Y > B && R < max(Y, B);
    bool bmax = B > Y && R < max(Y, B);
    
    if(ymax){
        swap(R, Y);
        swap(G, V);
        swap(table[0], table[2]);
        swap(table[3], table[5]);
    }
    if(bmax){
        swap(R, B);
        swap(G, O);
        swap(table[0], table[4]);
        swap(table[3], table[1]);
    }
    
    vector<int> vec;
    for(int i=0; i<R; i++)
        vec.push_back(0);
    for(int i=0; i<Y; i++){
        if(i < R)
            vec.insert(vec.begin()+i*2+1, 2);
        else
            vec.push_back(2);
    }
    reverse(vec.begin(), vec.end());
    for(int i=0; i<B; i++){
        if(i < R+Y)
            vec.insert(vec.begin()+i*2, 4);
        else
            vec.insert(vec.begin(), 4);
    }

    for(int i=0; i<vec.size(); i++){
        if(vec[i] == 0){
            for(int j=0; j<G; j++){
                vec.insert(vec.begin()+i, 3);
                vec.insert(vec.begin()+i, 0);
            }
            break;
        }
    }
    for(int i=0; i<vec.size(); i++){
        if(vec[i] == 2){
            for(int j=0; j<V; j++){
                vec.insert(vec.begin()+i, 5);
                vec.insert(vec.begin()+i, 2);
            }
            break;
        }
    }
    for(int i=0; i<vec.size(); i++){
        if(vec[i] == 4){
            for(int j=0; j<O; j++){
                vec.insert(vec.begin()+i, 1);
                vec.insert(vec.begin()+i, 4);
            }
            break;
        }
    }
        
    string res = "";
    for(auto v: vec)
        res += table[v];
    return res;
}

int main(){
    int T; cin >> T;
    for(int i=0; i<T; i++){
        cout << "Case #" << i+1 << ": ";
        cin >> N;
        cin >> R >> O >> Y >> G >> B >> V;
        
        cout << solve() << endl;
    }
    return 0;
}

C

略解

まず1頭の馬だけを使った場合の最小時間を求め、その後任意の馬を使った場合の最小時間を求める。

証明？

正直この問題は証明が殆ど存在しないと思う……

  1. 任意の2点間を1頭の馬だけを使って移動する場合の最小時間を求める。 Warshall-Floydで全点対最短経路を求めた後、始点の馬で移動できる場合はその場合に掛かる時間で更新する。

  2. 任意の2点間を任意の馬を使って移動する場合の最小時間を求める。 1により任意の2点間を1頭の馬だけを使い移動する場合の最小時間の配列が求まっている。 これを用いて同様にWarshall-Floydをすると任意の馬を使った場合の最小時間が求まる。

#define _LIBCPP_DEBUG 0
#include <bits/stdc++.h>
using namespace std;

typedef long long ll;

int N, Q;
vector<double> E, S;
vector<vector<ll>> D;

void solve(){
    for(int k=0; k<N; k++){
        for(int i=0; i<N; i++){
            for(int j=0; j<N; j++) if(D[i][k] != -1 && D[k][j] != -1){
                if(D[i][j] == -1)
                    D[i][j] = D[i][k] + D[k][j];
               else
                    D[i][j] = min(D[i][j], D[i][k] + D[k][j]);
            }
        }
    }
    vector<vector<double>> nD(N, vector<double>(N, 1e100));
    for(int i=0; i<N; i++){
        for(int j=0; j<N; j++) if(D[i][j] != -1 && D[i][j] <= E[i]){
            nD[i][j] = min(nD[i][j], D[i][j]/S[i]);
        }
    }
    for(int k=0; k<N; k++)
        for(int i=0; i<N; i++)
            for(int j=0; j<N; j++)
                nD[i][j] = min(nD[i][j], nD[i][k] + nD[k][j]);
    for(int i=0; i<Q; i++){
        int s, t;
        cin >> s >> t; s--; t--;
        cout << " " << nD[s][t];
    }
    cout << endl;
}

int main(){
    cout.precision(16);
    cout.setf(ios::fixed);
    
    int T; cin >> T;
    for(int i=0; i<T; i++){
        cout << "Case #" << i+1 << ":";
        cin >> N >> Q;
        E.resize(N);
        S.resize(N);
        for(int i=0; i<N; i++)
            cin >> E[i] >> S[i];
        D.clear();
        
        for(int i=0; i<N; i++){
            vector<ll> vec(N);
            for(int j=0; j<N; j++){
                cin >> vec[j];
            }
            D.push_back(vec);
        }
        solve();
    }
    
    return 0;
}

Nintendo Challenge解いた

まーす氏が突然問題を送ってきた。

https://www.nerd.nintendo.com/files/HireMe.cpp

実は初日で解法分かってたのにプログラムにバグが有って数バイト書き換えたら出来てクッソしょんぼり。

// https://www.nerd.nintendo.com/files/HireMe.cpp
#include <string.h>
#include <stdio.h>

typedef unsigned char u8;
typedef unsigned int u32;

u8 confusion[512]={
0xac,0xd1,0x25,0x94,0x1f,0xb3,0x33,0x28,0x7c,0x2b,0x17,0xbc,0xf6,0xb0,0x55,0x5d,
0x8f,0xd2,0x48,0xd4,0xd3,0x78,0x62,0x1a,0x02,0xf2,0x01,0xc9,0xaa,0xf0,0x83,0x71,
0x72,0x4b,0x6a,0xe8,0xe9,0x42,0xc0,0x53,0x63,0x66,0x13,0x4a,0xc1,0x85,0xcf,0x0c,
0x24,0x76,0xa5,0x6e,0xd7,0xa1,0xec,0xc6,0x04,0xc2,0xa2,0x5c,0x81,0x92,0x6c,0xda,
0xc6,0x86,0xba,0x4d,0x39,0xa0,0x0e,0x8c,0x8a,0xd0,0xfe,0x59,0x96,0x49,0xe6,0xea,
0x69,0x30,0x52,0x1c,0xe0,0xb2,0x05,0x9b,0x10,0x03,0xa8,0x64,0x51,0x97,0x02,0x09,
0x8e,0xad,0xf7,0x36,0x47,0xab,0xce,0x7f,0x56,0xca,0x00,0xe3,0xed,0xf1,0x38,0xd8,
0x26,0x1c,0xdc,0x35,0x91,0x43,0x2c,0x74,0xb4,0x61,0x9d,0x5e,0xe9,0x4c,0xbf,0x77,
0x16,0x1e,0x21,0x1d,0x2d,0xa9,0x95,0xb8,0xc3,0x8d,0xf8,0xdb,0x34,0xe1,0x84,0xd6,
0x0b,0x23,0x4e,0xff,0x3c,0x54,0xa7,0x78,0xa4,0x89,0x33,0x6d,0xfb,0x79,0x27,0xc4,
0xf9,0x40,0x41,0xdf,0xc5,0x82,0x93,0xdd,0xa6,0xef,0xcd,0x8d,0xa3,0xae,0x7a,0xb6,
0x2f,0xfd,0xbd,0xe5,0x98,0x66,0xf3,0x4f,0x57,0x88,0x90,0x9c,0x0a,0x50,0xe7,0x15,
0x7b,0x58,0xbc,0x07,0x68,0x3a,0x5f,0xee,0x32,0x9f,0xeb,0xcc,0x18,0x8b,0xe2,0x57,
0xb7,0x49,0x37,0xde,0xf5,0x99,0x67,0x5b,0x3b,0xbb,0x3d,0xb5,0x2d,0x19,0x2e,0x0d,
0x93,0xfc,0x7e,0x06,0x08,0xbe,0x3f,0xd9,0x2a,0x70,0x9a,0xc8,0x7d,0xd8,0x46,0x65,
0x22,0xf4,0xb9,0xa2,0x6f,0x12,0x1b,0x14,0x45,0xc7,0x87,0x31,0x60,0x29,0xf7,0x73,
0x2c,0x97,0x72,0xcd,0x89,0xa6,0x88,0x4c,0xe8,0x83,0xeb,0x59,0xca,0x50,0x3f,0x27,
0x4e,0xae,0x43,0xd5,0x6e,0xd0,0x99,0x7b,0x7c,0x40,0x0c,0x52,0x86,0xc1,0x46,0x12,
0x5a,0x28,0xa8,0xbb,0xcb,0xf0,0x11,0x95,0x26,0x0d,0x34,0x66,0x22,0x18,0x6f,0x51,
0x9b,0x3b,0xda,0xec,0x5e,0x00,0x2a,0xf5,0x8f,0x61,0xba,0x96,0xb3,0xd1,0x30,0xdc,
0x33,0x75,0xe9,0x6d,0xc8,0xa1,0x3a,0x3e,0x5f,0x9d,0xfd,0xa9,0x31,0x9f,0xaa,0x85,
0x2f,0x92,0xaf,0x67,0x78,0xa5,0xab,0x03,0x21,0x4f,0xb9,0xad,0xfe,0xf3,0x42,0xfc,
0x17,0xd7,0xee,0xa3,0xd8,0x80,0x14,0x2e,0xa0,0x47,0x55,0xc4,0xff,0xe5,0x13,0x3f,
0x81,0xb6,0x7a,0x94,0xd0,0xb5,0x54,0xbf,0x91,0xa7,0x37,0xf1,0x6b,0xc9,0x1b,0xb1,
0x3c,0xb6,0xd9,0x32,0x24,0x8d,0xf2,0x82,0xb4,0xf9,0xdb,0x7d,0x44,0xfb,0x1e,0xd4,
0xea,0x5d,0x35,0x69,0x23,0x71,0x57,0x01,0x06,0xe4,0x55,0x9a,0xa4,0x58,0x56,0xc7,
0x4a,0x8c,0x8a,0xd6,0x6a,0x49,0x70,0xc5,0x8e,0x0a,0x62,0xdc,0x29,0x4b,0x42,0x41,
0xcb,0x2b,0xb7,0xce,0x08,0xa1,0x76,0x1d,0x1a,0xb8,0xe3,0xcc,0x7e,0x48,0x20,0xe6,
0xf8,0x45,0x93,0xde,0xc3,0x63,0x0f,0xb0,0xac,0x5c,0xba,0xdf,0x07,0x77,0xe7,0x4e,
0x1f,0x28,0x10,0x6c,0x59,0xd3,0xdd,0x2d,0x65,0x39,0xb2,0x74,0x84,0x3d,0xf4,0xbd,
0xc7,0x79,0x60,0x0b,0x4d,0x33,0x36,0x25,0xbc,0xe0,0x09,0xcf,0x5b,0xe2,0x38,0x9e,
0xc0,0xef,0xd2,0x16,0x05,0xbe,0x53,0xf7,0xc2,0xc6,0xa2,0x24,0x98,0x1c,0xad,0x04};

u32 diffusion[32]={
0xf26cb481,0x16a5dc92,0x3c5ba924,0x79b65248,0x2fc64b18,0x615acd29,0xc3b59a42,0x976b2584,
0x6cf281b4,0xa51692dc,0x5b3c24a9,0xb6794852,0xc62f184b,0x5a6129cd,0xb5c3429a,0x6b978425,
0xb481f26c,0xdc9216a5,0xa9243c5b,0x524879b6,0x4b182fc6,0xcd29615a,0x9a42c3b5,0x2584976b,
0x81b46cf2,0x92dca516,0x24a95b3c,0x4852b679,0x184bc62f,0x29cd5a61,0x429ab5c3,0x84256b97};

//u8 input[32]={
////change only this :
//0x66,0xd5,0x4e,0x28,0x5f,0xff,0x6b,0x53,0xac,0x3b,0x34,0x14,0xb5,0x3c,0xb2,0xc6,
//0xa4,0x85,0x1e,0x0d,0x86,0xc7,0x4f,0xba,0x75,0x5e,0xcb,0xc3,0x6e,0x48,0x79,0x8f
////
//};

u8 input[32] = {155, 246, 61, 32, 15, 133, 115, 86, 141, 81, 144, 145, 255, 191, 104, 115, 134, 60, 190, 173, 242, 65, 252, 44, 146, 109, 80, 4, 19, 106, 217, 180};

void Forward(u8 c[32],u8 d[32],u8 s[512],u32 p[32])
{
    for(u32 i=0;i<256;i++)
    {
        for(u8 j=0;j<32;j++)
        {
            d[j]=s[c[j]];
            c[j]=0;
        }

        for(u8 j=0;j<32;j++)
            for(u8 k=0;k<32;k++)
                c[j]^=d[k]*((p[j]>>k)&1);
    }
    for(u8 i=0;i<16;i++)
        d[i]=s[c[i*2]]^s[c[i*2+1]+256];
}

int main(int argc, char* argv[])
{
    // u8 target[]="Hire me!!!!!!!!";
    u8 target[]="youjodepoyopoyo";
    u8 output[32];

    Forward(input,output,confusion,diffusion);

    printf("%s\n", output);
    return memcmp(output,target,16); // => contact jobs(at)nerd.nintendo.com
}