我眼中的形式化验证(2) - 用Verus验证Rust程序
形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。 这篇文章，我打算用Verus验证的例子，来讲一下‘定理证明’这个技术分支。Verus[1]这个...
我眼中的形式化验证(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了，你真的会来么？问我：我们学校今年迁新...
4G/5G网络IMP4GT中间人攻击风险分析
原文首发于公号“ 支付宝安全实验室” (https://mp.weixin.qq.com/s/lLrKx5VvSlnvyQDwK6TPug) 1分钟摘要德国波鸿鲁尔大学的研究人员在NDSS2020会议发表了一篇论文，提出了一种新的IMP4GT攻击方法...