上周末的 SECCON CTF, 有几个 QR 码的题..

Problem 1

http://www.youtube.com/watch?v=omobhuutrE4

这个视频里, 中间最下方有一个滚动的被挡住的 QR 二维码.

上学期组团参加了 SIGMOD Programming Contest 2014, 进入了 Finalist. 因此 6 月 23 日至 26 日, 我在 Utah 州 Snowbird 度假村参加 ACM SIGMOD/PODS 2014 会议.

每年的比赛题目跟 ACM-ICPC 比较像, 就是给输入, 产生确定的输出. 比赛形式的不同在于, ICPC 中选手要尽量快的写出一个运行速度可以接受的程序, 而在 SIGMOD 比赛里, 我们需要在一个多月时间里写出一个在给定机器上运行速度尽量快的程序, 而且可以用任何手段 (并行, 汇编, SIMD, 文件读写).

最终结果与之前的 online 测试结果基本一致, 获得了第四名. 听了其他选手的报告, 深深的感觉到, 压榨程序效率时, 算法并不怎么重要.

Problem

微信的聊天记录导出一直是挺麻烦的事, 尤其是在 iphone 上. 前几天想导出一部分语音聊天记录, 就到 iphone 的文件系统里去找了一下, 发现微信的语音记录存放在/var/mobile/Applications/{app id}/Documents/{user id}/Audio/{friend id}/*.aud

问题是, 微信将两人互相的对话音频存在一个目录下, 不知道如何区分, 去逆向微信的聊天记录格式恐怕比较困难, 于是想到使用上学期做的说话人识别 (Speaker Recognition) 系统来自动处理这个问题.

受人蛊惑拉拢, 3 月 8 号 8 点至 10 号 8 点, 我参加了首届「百度杯」全国网络安全技术对抗赛 (BCTF) 资格赛. 大家全都是第一次参加 CTF, 发觉自己实在各种弱, 不过长了很多见识.. 也遇到很多好玩的题目.

我们工具都不太专业, 尤其是二进制能力比较差, 之前从来都没用过 IDA, 没配过 gdb, Reverse/PWN 的题都只做出了最简单的. Web 题方面也没什么经验, 有提示的题能跟着线索做, 其余的都茫然了. Day1 和 Day2 上午我们队都曾到过 leaderboard top1. 不过慢慢被追上来了. CRYPTO500 如果不被坑的话早点做出来可能还有进决赛的希望..

随便说几个题好了..

贵系今年学生节海报谜题:

一些增加生活质量的, 软件层面的硬件使用:

Keyboard Mapping

CapsLock 是个大 bug, 十分不常用 (其实是完全可以不用), 但占了一块好位置, 还比别的键大, 简直不能忍.

尽管 BIOS 里能将 Left Ctrl 与 Fn 互换, 如果能把 CapsLock 映射到 Ctrl 的话, 对生活质量仍然是有极大提高的, 毕竟 Ctrl 太常用了, 对不写代码的人也是一样 (但是不写代码的人不用 Linux 吧..). 我们可以用xmodmap 工具来实现这一点.

最近又看了看光线追踪..

Theory

上回提到, Path Tracing 就是在试图解 Kajiya 86 年提出的渲染方程:

std::tuple 是 C++11 中的一个好东西. 它功能上算是std::pair 的扩展, 但有一些其他的用法.

例如, 可以借用 tuple 来模拟多值返回 (Python 中也是这样), SugarCpp 中就是使用 tuple 实现了简洁的多值返回语法:

tuple<T, T> sort<T>(a: T, b: T)
    return a < b ? (a, b) : (b, a)

tuple 也可以用于模拟 Python 中的 Parallel Assignment:

本来只想转 Joel 的那篇文章的, 不过不小心就转多了. 于是变成 Java 黑合集. 欢迎补充

maskray 提供了一个汇集了黑 Java 笑话的页面..

注: 本文只是开心的吐槽一下 Java 的一些缺点, 它的优点是值得承认的. 另外去 Google 实习了之后尤其觉得 Java 是可以写的很高端的.

The Peris of JavaSchools - Joel Spolsky

英文原文地址, 中文版地址, 译者阮一峰.

前些日子查资料的时候发现逻辑学家 George Boolos (不是 boolean 类型的 George Boole) 曾经给出过 Gödel 定理的一个新证明. 看了之后觉得十分有趣.

Review of Gödel's Proof

关于 Gödel 的原始证明, 网上已有许多解释, 如刘未鹏的这篇文章. 这里再从数理逻辑角度简单回顾一下, 因为 Boolos 的证明用了许多 Gödel 的思想.

证明的第一步是建立 Gödel Numbering, 也即建立一套编码系统, 使得形式系统中任意公式可与自然数一一对应. 这种思想及其方法在有了计算机的今天是十分轻易的, 在 Gödel 的文章里, 他用了不同素数表示形式系统中的最基本符号, 从而实现了这一点, 这种方法后来被称为 Gödel Numbering.