首页
社区
课程
招聘
问答 CTF 排行榜 知识库 工具下载 峰会 看雪商城 证书查询
  1. 社区
  2. 加壳脱壳
    3. 发新帖
[原创]备忘录：一些逻辑运算的公式推导（VMP、OLLVM）
发表于: 2019-2-19 16:32 18104

[原创]备忘录：一些逻辑运算的公式推导（VMP、OLLVM）

天水姜伯约 活跃值
4
2019-2-19 16:32
18104

a = b & c=>a = (b ^ ~c) & b

a = b | c=>a = (b & c) | (b ^ c)

a = a ^ b=>a = (~a & b) | (a & ~b)

知识点：命题逻辑 - > 等值演算

下文中nand应修改为nor！

万用门其实就是数字电路中的与非门，一般是用Nand表示。

Nand(a,b) = ~a & ~b

Not(a) = ~a = ~a & ~a = Nand(a,a)

Or(a,b) = a | b = ~(~a & ~b) = Nand(Nand(a,b),Nand(a,b))

And(a,b) = a & b = ~~a & ~~b = Nand(Nand(a,a),Nand(b,b))

Xor(a,b) = (~a & b) | (a & ~b) = (0 | (a & ~b)) | (0 | (b & ~a)) = (a & (~a | ~b)) | (b & (~a | ~b)) = (~a | ~b) & (a | b) = ~(a & b) | ~(~a & ~b) = Nand(And(a,b),Nand(a,b)) = Nand(Nand(Nand(a,a),Nand(b,b)),Nand(a,b))

-a = ~a + 1

a - b = ~(a - b) + 1 = ~(a - b - 1) = ~(~a + 1 - 1 + b) = ~(~a + b)

减法公式的证明只能说是“自我安慰”，因为我不清楚如何证明其EFLAGS的得到过程。

OLLVM的指令替代混淆：

a = b & c=>a = (b ^ ~c) & b

证明过程：

Nand(a,b) = ~a & ~b

Not(a) = ~a = ~a & ~a = Nand(a,a)

Or(a,b) = a | b = ~(~a & ~b) = Nand(Nand(a,b),Nand(a,b))

And(a,b) = a & b = ~~a & ~~b = Nand(Nand(a,a),Nand(b,b))

Xor(a,b) = (~a & b) | (a & ~b) = (0 | (a & ~b)) | (0 | (b & ~a)) = (a & (~a | ~b)) | (b & (~a | ~b)) = (~a | ~b) & (a | b) = ~(a & b) | ~(~a & ~b) = Nand(And(a,b),Nand(a,b)) = Nand(Nand(Nand(a,a),Nand(b,b)),Nand(a,b))

-a = ~a + 1

a - b = ~(a - b) + 1 = ~(a - b - 1) = ~(~a + 1 - 1 + b) = ~(~a + b)

减法公式的证明只能说是“自我安慰”，因为我不清楚如何证明其EFLAGS的得到过程。
Nand(a,b) = ~a & ~b

Not(a) = ~a = ~a & ~a = Nand(a,a)

Or(a,b) = a | b = ~(~a & ~b) = Nand(Nand(a,b),Nand(a,b))

And(a,b) = a & b = ~~a & ~~b = Nand(Nand(a,a),Nand(b,b))

[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课

最后于 2019-2-22 22:20 被天水姜伯约编辑 ，原因：
收藏
免费 ・1
支持
分享
打赏 + 1.00雪花
Editor
打赏次数 1 雪花 + 1.00
 
赞赏  Editor   +1.00 2019/02/21 感谢分享～
最新回复 (10)
xiaohang
雪    币： 2166
活跃值： (3226)
能力值： (RANK：260 )
在线值：
发帖
回帖
粉丝
私信
2 楼
可以收藏一下，这个知识点还是很有用的
2019-2-20 01:01
0
MsScotch
雪    币： 3181
活跃值： (1796)
能力值： ( LV2，RANK：10 )
在线值：
发帖
回帖
粉丝
私信
3 楼
这个真心有帮到，多谢。
2019-2-20 13:00
0
如斯咩咩咩
雪    币： 4709
活跃值： (1575)
能力值： ( LV2，RANK：15 )
在线值：
发帖
回帖
粉丝
私信
4 楼
Get 学习
2019-2-20 16:06
0
月落之汀
雪    币： 6369
活跃值： (1688)
能力值： ( LV4，RANK：156 )
在线值：
发帖
回帖
粉丝
私信
5 楼
lz，关于ollvm，我之前想基于ir对它做静态去混淆，但卡在了表达式化简上，ollvm原版的几种固定模式还好说，但定制版的ollvm都是自己定制了这种表达式，不通过符号执行的话，很难做到通用，我之前的思路是能不能用z3一类的库进行表达式化简呢？但苦于没法证实想法是否正确
最后于 2019-2-21 14:07 被月落之汀编辑 ，原因：
2019-2-21 08:13
1
Editor
雪    币： 26245
活跃值： (63297)
能力值： (RANK：135 )
在线值：
发帖
回帖
粉丝
私信
6 楼
多谢大表哥
2019-2-21 14:15
0
Anskya
雪    币： 1272
活跃值： (746)
能力值： ( LV13，RANK：810 )
在线值：
发帖
回帖
粉丝
私信
7 楼
Nand(a,b) = ~a & ~b
根据德摩根定律，其实是NOR而不是NAND
NAND = ~(a & b) = ~a | ~b

另外不管是NOR,NAND都是很古老的知识，实际上万用门很多很多，不要局限于《布尔代数》
2019-2-22 19:49
0
天水姜伯约
雪    币： 2635
活跃值： (5083)
能力值： ( LV9，RANK：225 )
在线值：
发帖
回帖
粉丝
私信
8 楼
月落之汀 lz，关于ollvm，我之前想基于ir对它做静态去混淆，但卡在了表达式化简上，ollvm原版的几种固定模式还好说，但定制版的ollvm都是自己定制了这种表达式，不通过符号执行的话，很难做到通用，我之前 ...
很抱歉，我也还在思考这个问题，无法给你确切有用的回复。
我的初步想法是生成一个逻辑运算表达式树，然后在里面用真值表将一些长逻辑运算表达式化简为and,or等。
2019-2-22 22:16
0
天水姜伯约
雪    币： 2635
活跃值： (5083)
能力值： ( LV9，RANK：225 )
在线值：
发帖
回帖
粉丝
私信
9 楼
Anskya Nand(a,b) = ~a & ~b 根据德摩根定律，其实是NOR而不是NAND NAND = ~(a & b) = ~a | ~b 另外不管是NOR,NAND都是很古老的 ...
感谢纠正错误。
2019-2-22 22:19
0
爆破鬼才FC
雪    币：
活跃值： (27)
能力值： ( LV2，RANK：10 )
在线值：
发帖
回帖
粉丝
私信
10 楼
Anskya Nand(a,b) = ~a & ~b 根据德摩根定律，其实是NOR而不是NAND NAND = ~(a & b) = ~a | ~b 另外不管是NOR,NAND都是很古老的 ...
我看看雪的10年的一篇文章，也是看了1天不懂为啥是Nand(a,b) = ~a & ~b，我觉得应该是个Nand(a,b) = ~a | ~b，谢谢7楼大佬分析。另附上我看的那篇链接http://bbs.pediy.com/showthread.php?t=121412 
2019-6-6 15:04
0
kakasasa
雪    币： 576
活跃值： (2035)
能力值： ( LV2，RANK：10 )
在线值：
发帖
回帖
粉丝
私信
11 楼
mark
2021-3-31 20:43
0
游客
登录 | 注册 方可回帖
回帖 表情 雪币赚取及消费
高级回复
返回
//