CertiK工程师专访|受邀参加今年EthCC的哲学派系研发工程师

今天要为大家介绍的是一位哲学家，他是来自CertiK的技术小伙伴中唯一一位主修了哲学专业的大神。

他在主修哲学时，对波兰数学家、逻辑学家塔斯基（Alfred Tarski ）1933年在《形式化语言中的真理概念》一文中提出了一个对于“真理”（Truth）的语义学定义十分感兴趣。这个语义学定义深刻地影响了20世纪逻辑经验主义和后来的分析哲学的意义理论，并且导致理论语义学的正式建立。

有趣的是，形式化语言一词，在计算机科学中同样存在。

形式化语言，所谓形式上正确的是指能将清晰、不会混淆的定义词项，精确、无歧义地用于被定义词项的外延。而在计算机科学中的Formal language，则同样是定义界限明确的，以无限的语言为研究对象，以有限的手段描述无限的语言。

在一步步的了解之下，他对计算机科学产生了浓厚的兴趣，因此主修了第二学位计算机——从此踏上了码农这条不归路。

工程师简介

孙信远（Xinyuan Sun)

CertiK研发工程师，来自中国南京，目前居住于美国纽约。

哲学、计算机双学位，于一年前加入CertiK。

主要业务为构建相关框架以扩展加密审计解决方案。

哲学与计算机中的“真理”

上文为大家提到了哲学方面的形式化语言，其实还有一些很有趣的小故事。在这里跟大家稍微发散一下。

在1933年，塔斯基提出对于“真理”（Truth）的语义学定义之前，德国数学家、逻辑学家和哲学家弗里德里希·路德维希·戈特洛布·弗雷格（......这名字也太长了）已经在这一领域摸索良久，他于1879年将其著作《算数的基本规则》完稿付印时，收到了英国数学家罗素寄出的一封信，信中就是大家耳熟能详的罗素悖论。

这个悖论是由罗素发现的一个集合论悖论，其基本思想是：对于任意一个集合A，A要么是自身的元素，即A∈A；A要么不是自身的元素，即A?A。根据康托尔集合论的概括原则，可将所有不是自身元素的集合构成一个集合S1，即S1={x:x?x}。

换个好理解一点的理论：理发师悖论。

某度有言：在某个城市中有一位理发师，他的广告词是这样写的：“本人的理发技艺十分高超，誉满全城。我将为本城所有不给自己刮脸的人刮脸，我也只给这些人刮脸。”

来找他刮脸的人络绎不绝，自然都是那些不给自己刮脸的人。可是，有一天，这位理发师从镜子里看见自己的胡子长了，他本能地抓起了剃刀，你们看他能不能给他自己刮脸呢？如果他不给自己刮脸，他就属于“不给自己刮脸的人”，他就要给自己刮脸，而如果他给自己刮脸呢？他又属于“给自己刮脸的人”，他就不该给自己刮脸。

弗雷格收到了罗素的信后：

他发现自己呕心沥血的证明结果被这条悖论折腾的一团糟，只好在书的末尾写道：“一个科学家所碰到的最倒霉的事，莫过于是在他的工作即将完成时却发现所做工作的基础崩溃了。”

罗素悖论引发基础数学形式化方法（公理化方法）的大普及，导致模型论的诞生，而后形式化语言定义逐渐发展成熟，这就是后话了。

言归正传，在学习哲学的时候看到这样的小故事很难不被笑到。

后来，他了解到计算机科学中也有同样的定义和词汇，怀揣着好奇心他推开了编码及研发的大门。都说兴趣是最好的老师，幸运的是，计算机带给孙信远的探索欲和思考与哲学同样多。

搭建乐高的乐趣

大学实习时有一次和老板闲聊，老板提到最近有个新团队——CertiK成立了，创始人是耶鲁大学计算机系系主任邵中教授和哥大计算机科学系顾荣辉教授，当时孙信远还未意识到这个团队将成为他的“本命”团队。

时间飞逝，孙信远很快就毕业了。

经朋友介绍，他接触到了顾教授实验室的小伙伴并开展了一些研发相关的合作。

随着对软件安全领域的认知逐渐加深，他期待加入CertiK的意愿也与日俱增。

CertiK的创始人邵中教授是研究编程语言、形式化验证、操作系统和软件安全等领域的领军人物，顾荣辉教授也是操作系统、软件安全以及形式化验证方面的专家。

对这两位教授的科研实力十分钦佩的孙信远终于鼓起勇气投递了简历。

事情进展的很顺利，他成功的加入了CertiK，成为了团队大神中的一员。

作为一名优秀的研发人员，很快他就投身CertiK各类产品和项目的开发过程中，参与开发了DeepSea编译器以及以下研究论文的撰写以及演讲：

除了以上research，孙信远还在做一些与DeFi攻击、DeFi金融模型监测，以及其他安全类的hypervisor的相关研究。在CertiK与蚂蚁金服合作的项目当中，孙信远也作为重要成员参与了该项目。

大家是否还记得下图：

CertiK曾在过去的一些攻击分析技术文章当中提及过金融模型漏洞一词——“即便代码没有漏洞，合约部署没有漏洞，问题也可能出在金融模型漏洞上”。

与其说检查金融模型，不如把搭建项目比作搭建乐高。因此DeFi也被称为“money lego”（金钱乐高）。

审计，就好比在搭建乐高的过程，检查每一个乐高块有无损坏，而DeFi金融模型的监测则是查看乐高是否存在非法搭建。

还有一个比较灵性的例子就是三只小猪的童话故事。

无论是三只小猪还是搭建乐高——DeFi的安全就像建筑的基底，坚实的材料和稳定的结构才能打好基础，优秀DeFi项目发展的每一步必然应为长远打算。

大家也可以持续关注CertiK官方公众号，关于DeFi金融模型的相关文章及小科普将会出现在之后的推文中哦。

EthCC 2021

加入CertiK以后，刚毕业的孙信远成长十分迅速。

一年紧张及充实的研发经历为他积累了丰厚的经验和优秀的专业技能。

时间来到现在——第四届以太坊社区会议EthCC 2021，向孙信远递出了邀请函。

他作为CertiK研发工程师，将于本周四7月22日北京时间19:05于会上进行主题为#以形式化验证为DeFi提供最高等级的安全解决方案#的演讲。

EthCC是欧洲最大的专注于技术和社区的年度以太坊活动，它由非营利性法国以太坊协会Asseth每年在巴黎组织，聚集了来自区块链生态系统的众多参与者，作为以开发人员为主题的大型会议吸引了全球以太坊和区块链社区的广泛关注。

本次会议一如往年，会上涵盖了包括安全在内的多个议题。

孙信远的此次演讲旨在和与会者一起分享DeFi技术层面的安全和发展，探讨如何使用DeepSEA来发现并防止两类黑客攻击#闪电贷攻击和价格预言机操纵攻击#，以及如何将这种方法扩展到DeFi协议的设计之上。

这次的受邀给了孙同学极大的成就感，这次的演讲也几近于将他踏入计算机行业以来的所有工作和研究进行了分类汇总、融会贯通，这就像是一张拼图最终完成的那种明朗和惬意！（学过哲学的工程师果然不太一样）

不正经问答

1. 每天日常都会做些什么？

宅在家工作，写一些research论文，参与一些技术会议，比如说这次的EthCC 2021。

另外平时很喜欢去移动餐车（food truck）吃鹰嘴豆泥（Hummus），毕竟国外好吃的不如国内多，这是附近我很喜欢的一家美食了。而且去food truck买东西还能为工作和research节约不少时间??

2. 听说工程师都挺喜欢养宠物的？

有一丢丢洁癖的我还是挺没法接受带毛的小动物的，不过要是没毛的话我会喜欢！

3. 有什么兴趣爱好吗？

疫情前会出去玩奥运反曲弓（Olympic Recurve）?

如果不工作不做research就读哲学书籍?

CertiK工程师专访到现在已经出了6期啦，如果你喜欢我们的团队，想要与大神们一起共事，欢迎快快投上你的简历加入我们！

如果你信任我们的技术大神，也欢迎随时通过微信公众号后台留言进行审计咨询免费获取审计时长及报价！

—-

编译者/作者：CertiK中文社区

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。