0. 总览 这是一篇过度冗长的博客，如果你有心情读，大不必都看，算是对我之前workshop paper的一个背景补充介绍。 什么是CFA 什么是AAM式的CFA算法 不同闭...
IP属地：纽约州
-
AAM 与 Control Flow Anlaysis中的精度控制 -
PL 2015 QE ProofPL QE2015 Claim For all expression , state and , and integer . If then there is a sta...
-
PL 2020-2 QE Prooforiginal question[https://eng-cs.syr.edu/wp-content/uploads/2020/09/CIS-exam-Jan-6-2020...
-
所以写显示的类型签名是一个比较好的习惯，并且合理的使用ide工具也是不错的选在。
求值和效率我觉得并没有什么直接的关系。 求值顺序是语义层面的，而效率是编译器层面。使用什么样的求值更多还是看语义设计所面向的想要解决的问题。来自地狱的杂技团----函数与函数类型
我在Structral programming and formal method 的前半部分简单的接触了Haskell的最基本的语法。 但是用haskell写出如此丑陋的代...
-
炼丹安全？一些胡思乱想
下面只是我的思考笔记，所以会非常自由和不严谨，不论是验证还是AI都不是我的研究方向，存在大量谬误 最近由于课程原因，我开始读一些神经网络相关的东西。 由于我本身的研究还是黑魔...
-
Something I fail to prove ......Pre I had thought I understand how to prove progress in Coq for some simple semantic...
-
安全信息流与2-safety性质
Pre 在之前的文章中我简单的介绍了一种描述计算机安全常用的方式: Non-interference模型(GMNI)。 再用一句话来回顾一下什么是non-intererenc...
-
当我们谈计算机安全的时候我们在谈什么(noninterference)
Pre 相信大家都学过不少关于计算机安全的课程和知识， 大家多多少少对各种各样的攻击方式有一定的了解。但是当谈及到底什么样的程序可以被认为是安全的时候， 这都不会是一个容易回...
-
Find C++ Thiscall in Binary
Backgrond: calling convention defines what register will be used to pass argument from ...
-
DDisasm Code Note
ELF loader Section some section might be useful. We can know what they are by some fla...
-
Dimension Shift! 一起来学Datalog吧！Pre 相信很多阅读龙书/PPA朋友在使用C++之类的语言实现书上的程序分析算法的时候会感觉到无比头疼， 甚至是在实现完成之后还是对算法稀里糊涂的。因为这些书在描述算法的时候...
-
知乎：<a href="https://links.jianshu.com/go?to=https%3A%2F%2Fwww.zhihu.com%2Fpeople%2Fthzt" target="_blank">https://www.zhihu.com/people/thzt</a><br>博客：<a href="https://links.jianshu.com/go?to=https%3A%2F%2Fthzt.github.io" target="_blank">https://thzt.github.io</a><br>文档：<a href="https://links.jianshu.com/go?to=https%3A%2F%2Fyuque.com%2Fthzt" target="_blank">https://yuque.com/thzt</a>
-
数据流分析(2) - 框架化分析 distributive framework之前我简单的介绍过几种常见的过程内分析算法。 可以看到这些算法有非常大的相似性，本质都是使用一个worklist里面存放需要分析的语句，再使用Kill/Gen 函数（或者说方...
-
Fuzz A Program!什么是Fuzz? 嘛这篇blog 还是会是一篇和计算机相关的Blog, 希望有机会我也能写一些和上面图里的Fuzzer相关的文章hhhhh 如何保证程序的正确性？ 相信每一个...
-
Structral Facts in Datalog: 一种更加理想的Datalog Syntax
什么是Datalog datalog是一种用于描述形如：u ⇐ p ∧ q ∧ … ∧ t的逻辑关系的一种一阶逻辑的声明式查询语言。这种形式的逻辑表达式也被称为Horn Cl...
-
数据流分析 (1) 过程内分析 Intraprocedural Analysis过程内分析，顾名思义， 不考虑任何的过程/函数间调用的分析算法。 总的来说，这是最基础也是最简单的一类程序分析算法， 但是其实还是比较有用， 特别是在二进制分析的实际应用中...
-
数据流分析 (0) : 示例语言和数据流数据流分析是一种比较经典的分析算法， 在大量的编译原理的书里都会提到（比如龙书）。在PPA 中，为了方便讨论，使用了一种非常简单的命令式语言作为示例来进行讲解。 Syntax...
-
PPA 读书笔记 0 ： Pre
这个笔记主要会记录我在实现PPA 中算法的时候遇到的一些问题， 可能不会放太多PPA书上已经有的内容。 初步计划是我会使用racket, 和逻辑式编程的方式(也许并不是某一种...
