我眼中的形式化验证(3) - 用Model Checking做协议验证
上周，我们在ASE 2025会议发表了论文“Securing Millions of Decentralized Identities in Alipay Super App with End-to-End Formal Verification”，...
我眼中的形式化验证(2) - 用Verus验证Rust程序
形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。 这篇文章，我打算用Verus验证的例子，来讲一下‘演绎证明’(Deductive Proof)...
我眼中的形式化验证(1) - 介绍一些经典案例
我给自己立了一个flag是年底之前完成一篇科普小作文，今天是12月31日，所以不管写成什么样，一定要贴出来 :) 什么是形式化验证？形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有...
Today’s Super-Apps, Security Challenges and Corresponding Paradigms
这是在CCS 2024会议的，Workshop on Secure and Trustworthy Superapps (SaTS)上我做的Keynote演讲的标题。演讲主要内容是分享了我们在小程序安全方面的经验与思考，总结了安全风险、挑战，应对方法...
面试和招聘的算法——2012年的诺贝尔经济学奖
竟然有1年多没有写东西！今天终于强迫自己更新了一篇。 我自己既是公司校招的面试官，也经历过自己孩子的小升初的过程。应聘者和招聘者的焦虑，我都深有体会。问我：我们学校是你们的唯一选择吗？我问：我们如果发offer了，你真的会来么？问我：我们学校今年迁新...