Group of Software Security In Progress

GoSSIP @ LoCCS.Shanghai Jiao Tong University

Analyzing Semantic Correctness With Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification

题目:Analyzing Semantic Correctness with Symbolic Execution: A Case Study on PKCS#1 v1.5 Signature Verification

作者:Sze Yiu Chau[1], Moosa Yahyazadehy[2], Omar Chowdhuryy[2], Aniket Kate[1], Ninghui Li[1]

单位:[1]Purdue University, [2]The University of Iowa

出处: The Network and Distributed System Security Symposium (NDSS) 2019

原文:https://www.ndss-symposium.org/wp-content/uploads/2019/02/ndss2019_04A-4_Chau_paper.pdf

/images/2019-04-21:会议:NDSS2019个人主页PPT


一、背景

密码协议是保证数据安全可靠的协议,在现代的各个领域中都具有不可代替的作用。但是,开发一个安全可靠的密码协议并不是一件容易的事情,把密码理论应用到实际的生产中需要经历漫长的开发过程,在这之中,即使有一点点的疏忽,也可能导致原来安全的密码协议变得不再安全。

来源于数学理论的密码结构,在假定的前提下,通常是很难破解的,而在实际中,这些密码结构通常需要使用一种中间结构来表示(Glue Protocol,本文中是指 PKCS#1 v1.5),以适应不同的输入数据和数据格式。

当密码协议设计好之后,就要按照设计说明书来实现它,以此来保证密码协议的安全性,倘若在实现过程中没有严格按照标准实现,就有可能达不到原来设定的安全等级,使得密码协议容易遭到各种攻击。

PKCS#1 v1.5 就是一种中间结构,在 RSA 算法中,PKCS#1 v1.5 定义了 RSA 的数学表示形式,在某些特殊的参数设定下(例如:使用较小的公钥指数 e),PKCS#1 v1.5 签名验证方案可以让攻击者在没有私钥、也不对模数进行分解的情况下伪造一个数字签名。

像 IPSec 中的密钥生成函数 ipsec_rsasigkey ,所生成的公钥指数 e = 3,而且没有任何选项可供选择(比如生成更大的公钥指数),再结合代码实现中对签名数据的处理不当(例如:在 Openswan 中),就使得签名信息容易被攻击者伪造,造成不必要的损失。因此,检查代码实现中的语义信息的正确性就变得一项重要的工作。

Gigahorse: Thorough, Declarative Decompilation of Smart Contracts

作者:Neville Grech, Lexi Brent, Bernhard Scholz, Yannis Smaragdakis

单位:University of Athens and University of Malta, The University of Sydney, University of Athens

出处:ICSE’19

原文:http://yanniss.github.io/gigahorse-icse19.pdf


Abstract

智能合约是运行在区块链上的应用程序,其具有自主交易加密货币和代币的能力。随着智能合约的飞速发展,各种各样的安全威胁也接踵而至。然而,由于智能合约是以非常底层的字节码的形式存储并运行在区块链上的,如何有效的针对智能合约进行复杂的程序分析已经成为了一个亟待解决的难题。

文章提出了Gigahorse工具链,其核心是一个能够将智能合约由EVM字节码反编译为三地址码的反编译器。反编译得到的中间代码能够显式的体现出原先EVM字节码中隐式的数据流和控制流依赖。Gigahorse通过使用一种基于逻辑的声明式规范,利用高层的语义理解指导底层的反编译过程,成功反编译了超过99.98%的已部署合约。此外,Gigahorse还提供了一套功能齐全的工具链,以用于进一步的程序分析。

Total Recall: Persistence of Passwords in Android

出处:NDSS 2019

作者:Jaeho Lee, Ang Chen and Dan S. Wallach

单位:Rice University

原文链接:https://www.ndss-symposium.org/wp-content/uploads/2019/02/ndss2019_06A-4_Lee_paper.pdf


文章概述

处理内存中敏感数据,比较安全的做法是一旦数据不再使用,便将敏感数据缓存清零。这样即使攻击者获得了设备物理内存快照(通过物理接触或者Meltdown、Spectre等攻击方式),也没办法获取到敏感数据内容。在本文中,作者将关注点放在内存中的用户密码(password)上,通过对安卓框架和不同App(包括流行App、密码管理App和系统锁屏程序)的深入分析,对安卓App的内存中密码数据残留情况进行了系统的研究。研究结果表明安卓App中密码数据残留的情况确实不容乐观。作者总结了各种密码数据残留的情况及其成因,提出了解决方案并对该方案进行了评估。

Spectre Attacks:Exploiting Speculative Execution

作者:Paul Kocher1 , Daniel Genkin2 , Daniel Gruss3 , Werner Haas4 , Mike Hamburg5 , Moritz Lipp3 , Stefan Mangard 3 , Thomas Prescher 4 , Michael Schwarz 3 , Yuval Yarom 6

单位:1 Independent, 2 University of Pennsylvania and University of Maryland, 3 Graz University of Technology,4 Cyberus Technology,5 Rambus, Cryptography Research Division,6 University of Adelaide and Data61

出处:S&P 19

链接:https://spectreattack.com/spectre.pdf


1.introduction

在当前,现代计算机在执行条件跳转指令时使用跳转预测和推测执行来提高执行速度。具体来说,在执行条件跳转指令时,cpu在无法迅速确认下一条需要执行的指令时,会尝试预测并继续执行,执行结果会被丢弃或者确认。但是预测逻辑并不可靠,在执行预测的指令时,cpu会对程序产生可见的side effect。这种方式造成的信息泄漏可以诱发一种幽灵攻击(specture attack)。
幽灵攻击吸引受害者程序在正常执行过程中预测执行部分代码,将受害者程序中的机密信息通过侧信道传输给攻击者。这种攻击可以被用来攻破程序隔离,jit编译,容器机制。

example

conditional branch

具体来说,对于如下代码,如果array1_size处于uncached状态,并且攻击者能够控制x,并且希望获取array1[x]中的机密信息。

if (x < array1_size)
    y = array2[array1[x] * 256]; 

在cpu执行条件判断时,由于array1_size不在cache中,cpu需要从memory中读取array1_size才能判断跳转是否成立。为了提高执行性能,cpu在经过攻击者的多次‘训练’后,认为会条件判断成立,执行赋值语句能够提高性能。cpu会保存当前寄存器状态进入checkpoint,并预测执行y = array2[array1[x] * 256],将array2[array1[x]*256]读入cache。
虽然过后寄存器状态被恢复到checkpoint,但cache状态已经发生了变化,攻击者可以通过flush&reload方法判断array1[x]的值,造成信息leak。

indirect branch

同样的攻击也能够通过间接跳转实现。攻击者通过‘训练’Branch Target Buffer (BTB)多次跳转到gadget的虚拟地址,令victim程序在执行时,cpu预测执行gadget代码。如果gadget被精心选择,攻击能够读取victim程序中的全部内存。

Data Oblivious ISA Extensions for Side Channel-Resistant and High Performance Computing

作者:Jiyong Yu, Lucas Hsiung, Mohamad El Hajj, Christopher W. Fletcher

单位:University of Illinois at Urbana-Champaign

会议:NDSS 2019

原文链接:https://www.ndss-symposium.org/wp-content/uploads/2019/02/ndss2019_05B-4_Yu_paper.pdf

摘要

  • 指出了现有Data Oblivious Code(秘密信息不会留下trace的程序,健忘的)的安全性问题和性能问题
  • 在BOOM(Berkeley Out-of-Order Machine)基础上设计了一个可乱序执行可预测执行(允许常见优化)的OISA
  • 可以证明达到了BitCycle级的路径不可分辨性
  • 进行了性能评估,证明其性能优势

DTaint: Detecting the Taint-Style Vulnerability in Embedded Device Firmware

作者:Kai Cheng, Qiang Li, Lei Wang, Qian Chen, Yaowen Zheng, Limin Sun, Zhenkai Liang

单位: Beijing Jiaotong University, University of Chinese Academy of Sciences, National University of Singapore

会议:DSN’18

原文:https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8416504


1 INTRODUCTION

作者提出了一种静态二进制分析方法DTaint,用于检测firmware中的污点漏洞。

由于很多厂商(90%)没有提供firmware的公开源码,并且制造商通常使用专有硬件组件定制固件,很难进行动态分析。

  • 动态分析

    作者使用FIRMADYNE——自动化固件动态分析系统,来分析2009-2016收集的firmware镜像,发现只有一小部分(少于670)firmware可以被模拟用于发现漏洞。

  • 污点式漏洞

    指的是由于对用户输入没有进行有效过滤,导致攻击者提供输入到达一个不安全的敏感位置,产生系统安全漏洞。例如,缓冲区溢出和命令行注入。发现该漏洞分为三个阶段:

    • 识别attacker-controlled sources。标记数据输入为tainted point,表示输入来源。
    • 识别security-sensitive sinks。标记不安全的库函数或代码作为sink,表示在这些位置数据可能会成为一个漏洞。
    • 找到漏洞作为不安全数据路径。获得输入和sink之间的数据传播过程,如果路径缺乏安全过滤,可以将其标记为不安全路径。
  • 特点:

    • 首次在设备固件的二进制代码中检查污点式漏洞
    • 与传统工具相比,DTaint可以检测更多的漏洞,使用更短的时间

Dangerous Skills: Understanding and Mitigating Security Risks of Voice-Controlled Third-Party Functions on Virtual Personal Assistant Systems

作者:Nan Zhang , Xianghang Mi , Xuan Feng , XiaoFeng Wang , Yuan Tian and Feng Qian

单位:Indiana University, Bloomington; Beijing Key Laboratory of IOT Information Security Technology, Institute of Information Engineering, CAS, China; University of Virginia

出处:IEEE S&P ‘19

原文:pdf


简介

VPA(virtual personal assistant):用户通过全语音与智能音箱进行交互获取服务,询问天气、播放音乐等,其中由第三方开发的功能叫做skill。

这篇文章研究了两个较为常见的VPA:Amazon Alexa, Google Assistant。

安全风险:涉及开放、嘈杂的声音信道没有有效的认证方式;让用户辨别交互的是正确的skill或VPA是困难的。

作者提出了两种攻击方式:

VSA (Voice Squatting Attack):口述指令的不同方式导致的攻击(口音和敬词的使用),比如“open Capital One please” –> 正常:Capital One;恶意:Capital One Please/Capital Won.

VMA (Voice Masquerading Attack):将用户的语音交给当前skill处理而不是VPA,假装退让控制权给其他服务或skill,收集用户的私密信息。

解决措施:

skill-name scanner:利用ARPABET的发音规则,检测发音相似或者存在子集关系的skill。

detector:检测skill模仿VPA的响应、解析用户意图是否有skill切换。

贡献:

第一次研究恶意skill的安全风险,提出了两种攻击方式,提出了减轻安全风险的技术。

Iodine: Fast Dynamic Taint Tracking Using Rollback-free Optimistic Hybrid Analysis

作者:Subarno Banerjee, David Devecsery † , Peter M. Chen and Satish Narayanasamy

单位:University of Michigan | Georgia Institute of Technology

出处:IEEE S&P 2019

资料:Paper


1. Abstract & Introduction

DIFT技术也称为动态污点分析 (Dynamic Taint Analysis) ,可以作为一个安全方案实施,但是实际并没有投入使用,原因就是过高的性能开销。DIFT效率低的原因是需要监控每一个指令,从而监控污点的传播。

本文中,作者提出了一个新的针对DIFT (Dynamic Information-flow Tracking) 的优化方法,叫做Iodine。这个新的技术基于OHA (Optimistic Hybrid Analysis)来减小DIFT的开销,同时不需要回滚(开销就小了)。

本文中作者主要和三种DIFT技术进行了对比: 1. 最原始的DIFT 2. 结合了保守静态分析的DIFT 3. 基于OHA的DIFT(指的就是结合了预测静态分析的DIFT)

作者的关键思路是限制预测静态分析 (Predicted Static Analysis) ,只删掉那些被证明是可以安全删除的monitor (即Safe Elision,作者后面还说明了Noop Elision即为Safe Elision),从而减少运行时的monitor,在保证性能的同时又保证稳定性,具体的预测静态分析采用的是预测前向污点分析以及传统的后向污点污点。这种思路下,程序事先运行时即使违背了预先假设的Invariant(预先的一些认为会成立的假设),也能正常执行。

The Rise of Certificate Transparency and Its Implications on the Internet Ecosystem

作者:Quirin Scheitle, Oliver Gasser, Theodor Nolte, Johanna Amann, Lexi Brent, Georg Carle, Ralph Holz, Thomas C. Schmidt, Matthias Wählisch

单位: TUM, HAW Hamburg, ICSI/Corelight/LBNL, The University of Sydney, FU Berlin

原文:link

出处:ACM IMC


Introduction

证书公开日志通过公开记录那些CA已经颁发证书,可以为互联网的域名拥有者提供监控自己证书发布情况的平台,意在及时发现恶意的证书颁发行为。

在2018年四月份,Chrome要求所有新颁布的证书都需要记录在证书公开日志中,随着证书公开日志的逐渐普及,一些问题也逐渐显现出来。本篇文章意在研究CT的普及情况,以及其公开透明性所可能产生的负面影响。

MicroWalk: A Framework for Finding Side Channels in Binaries

作者:Jan Wichelmann, Ahmad Moghimi, Thomas Eisenbarth, and Berk Sunar

单位:Universität zu Lübeck, Worcester Polytechnic Institute

链接:https://arxiv.org/pdf/1808.05575.pdf

会议:ACSAC ’18


1.摘要

研究背景:攻击者可能通过微架构(cache等)侧信道方式获取密钥,因此能够非人工检测出此类侧信道方式是有意义的。 1. 分析对象:选择software binaries,而不是source code的原因在于 binary运行时存在的信息泄露问题 在source code中观察不到。一些商业密码软件没有公布源码。 2. 分析方向:基于memory和control-flow的side-channel。
3. 分析方法:基于Dynamic Binary Instrumentation以及Mutual Information Analysis