More Like this

1. Young children’s drawings and descriptions of layouts and objects.

   https://doi.org/10.31234/osf.io/drfex  

   Bochynska, Agata; Dillon, Moira R. (January 2022, Proceedings of the Annual Meeting of the Cognitive Science Society)

   Young children tend to prioritize objects over layouts in their drawings, often juxtaposing “floating” objects in the picture plane instead of grounding those objects in drawn representations of the extended layout. In the present study, we explore whether implicitly directing children’s attention to elements of the extended layout through a drawing’s communicative goal—to indicate the location of a hidden target to someone else—might lead children to draw more layout information. By comparing children’s drawings to a different group of children’s verbal descriptions, moreover, we explore how communicative medium affects children’s inclusion of layout and object information. If attention modulates children’s symbolic communication about layouts and objects, then children should both draw and talk about layouts and objects when they are relevant to the communicative task. If there are challenges or advantages specific to either medium, then children might treat layouts and objects differently when drawing versus describing them. We find evidence for both of these possibilities: Attention affects what children include in symbolic communication, like drawings and language, but children are more concise in their inclusion of relevant layout or object information in language versus drawings. 

   more » « less
2. Quantitative Symbolic Similarity Analysis

   https://doi.org/10.1145/3597926.3605238  

   Sarker, Laboni (July 2023, ACM)

   Similarity analysis plays a crucial role in various software engineering tasks, such as detecting software changes, version merging, identifying plagiarism, and analyzing binary code. Equivalence analysis, a stricter form of similarity, focuses on determining whether different programs or versions of the same program behave identically. While extensive research exists on code and binary similarity as well as equivalence analysis, there is a lack of quantitative reasoning in these areas. Non-equivalence is a spectrum that requires deeper exploration, as it can manifest in different ways across the input domain space. This paper emphasizes the importance of quantitative reasoning on non-equivalence which arises due to semantic differences. By quantitatively reasoning about non-equivalence, it becomes possible to identify specific input ranges for which programs are equivalent or non-equivalent. We aim to address the gap in quantitative reasoning in symbolic similarity analysis, enabling a more comprehensive understanding of program behavior. 

   more » « less
3. Foundational Integration Verification of a Cryptographic Server

   https://doi.org/10.1145/3656446  

   Erbsen, Andres; Philipoom, Jade; Jamner, Dustin; Lin, Ashley; Gruetter, Samuel; Pit-Claudel, Clément; Chlipala, Adam (June 2024, Proceedings of the ACM on Programming Languages)

   We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks. 

   more » « less
4. Soft-Output Joint Channel Estimation and Data Detection using Deep Unfolding

   https://doi.org/10.1109/ITW48936.2021.9611404  

   Song, Haochuan; You, Xiaohu; Zhang, Chuan; Studer, Christoph (October 2021, IEEE Information Theory Workshop (ITW))

   We propose a novel soft-output joint channel estimation and data detection (JED) algorithm for multiuser (MU) multiple-input multiple-output (MIMO) wireless communication systems. Our algorithm approximately solves a maximum a-posteriori JED optimization problem using deep unfolding and generates soft-output information for the transmitted bits in every iteration. The parameters of the unfolded algorithm are computed by a hyper-network that is trained with a binary cross entropy (BCE) loss. We evaluate the performance of our algorithm in a coded MU-MIMO system with 8 basestation antennas and 4 user equipments and compare it to state-of-the-art algorithms separate channel estimation from soft-output data detection. Our results demonstrate that our JED algorithm outperforms such data detectors with as few as 10 iterations. 

   more » « less
5. MalwareHunt: Semantics-Based Malware Diffing Speedup by Normalized Basic Block Memoization

   Ming, Jiang; Xu, Dongpeng; Wu, Dinghao (August 2017, Journal of computer virology and hacking techniques)

   The key challenge of software reverse engi- neering is that the source code of the program under in- vestigation is typically not available. Identifying differ- ences between two executable binaries (binary diffing) can reveal valuable information in the absence of source code, such as vulnerability patches, software plagiarism evidence, and malware variant relations. Recently, a new binary diffing method based on symbolic execution and constraint solving has been proposed to look for the code pairs with the same semantics, even though they are ostensibly different in syntactics. Such semantics- based method captures intrinsic differences/similarities of binary code, making it a compelling choice to analyze highly-obfuscated malicious programs. However, due to the nature of symbolic execution, semantics-based bi- nary diffing suffers from significant performance slow- down, hindering it from analyzing large numbers of malware samples. In this paper, we attempt to miti- gate the high overhead of semantics-based binary diff- ing with application to malware lineage inference. We first study the key obstacles that contribute to the performance bottleneck. Then we propose normalized basic block memoization to speed up semantics-based binary diffing. We introduce an unionfind set structure that records semantically equivalent basic blocks. Managing the union-find structure during successive comparisons allows direct reuse of previously computed results. Moreover, we utilize a set of enhanced optimization methods to further cut down the invocation numbers of constraint solver. We have implemented our tech- nique, called MalwareHunt, on top of a trace-oriented binary diffing tool and evaluated it on 15 polymorphic and metamorphic malware families. We perform intra- family comparisons for the purpose of malware lineage inference. Our experimental results show that Malware- Huntcan accelerate symbolic execution from 2.8X to 5.3X (with an average 4.1X), and reduce constraint solver invocation by a factor of 3.0X to 6.0X (with an average 4.5X). 

   more » « less