SearcharxivSearch

arXiv subjects

Ali Ranjbar

Publications and source records attributed to Ali Ranjbar.

4 recordsLinked to original sources

VUPER: Verified ASN.1 UPER Parser

ASN.1 is a widely used interface description language, and UPER (Unaligned Packed Encoding Rules) is one of its key encoding rules, particularly popular in security-critical domains such as cellular networks and vehicle-to-everything (V2X) communication. To ensure the correctness and security of this foundational infrastructure, we present VUPER, a framework for generating verified ASN.1 UPER parsers. We first formalize the notion of a bit-precise parser and identify properties that prove round-trip consistency for parsers and serializers, while accounting for ASN.1 features such as backward/forward compatibility. We then implement and verify parser and serializer combinators for ASN.1 basic types and structures, while adhering to the UPER specification. We also develop a compiler that translates ASN.1 definitions into verified parsers. Finally, we develop a dynamic testing framework using the VUPER parser as a test oracle. To empirically evaluate our approach, we test 7 open-source and 4 commercial ASN.1 parsers using 5G and V2X communication protocols. VUPER uncovers 20 types of inconsistencies in popular parsers and demonstrates stricter compliance with ASN.1 UPER standards. Additionally, we demonstrate concrete attacks by exploiting these parser vulnerabilities.

cs.CR

LogicEval: A Systematic Framework for Evaluating Automated Repair Techniques for Logical Vulnerabilities in Real-World Software

Logical vulnerabilities in software stem from flaws in program logic rather than memory safety, which can lead to critical security failures. Although existing automated program repair techniques primarily focus on repairing memory corruption vulnerabilities, they struggle with logical vulnerabilities because of their limited semantic understanding of the vulnerable code and its expected behavior. On the other hand, recent successes of large language models (LLMs) in understanding and repairing code are promising. However, no framework currently exists to analyze the capabilities and limitations of such techniques for logical vulnerabilities. We aim to systematically evaluate both traditional and LLM based repair approaches for addressing real world logical vulnerabilities. To facilitate our assessment, we created the first ever dataset, LogicDS, comprising 122 logical vulnerabilities that reflect tangible security impact. We also developed a systematic framework, LogicEval, to evaluate patches for logical vulnerabilities. Evaluations suggest that compilation and testing failures are primarily driven by prompt sensitivity, loss of code context, and difficulty in patch localization.

cs.CR

FPGA-Based Multiplier with a New Approximate Full Adder for Error-Resilient Applications

Electronic devices primarily aim to offer low power consumption, high speed, and a compact area. The performance of very large-scale integration (VLSI) devices is influenced by arithmetic operations, where multiplication is a crucial operation. Therefore, a high-speed multiplier is essential for developing any signal-processing module. Numerous multipliers have been reviewed in existing literature, and their speed is largely determined by how partial products (PPs) are accumulated. To enhance the speed of multiplication beyond current methods, an approximate adder-based multiplier is introduced. This approach allows for the simultaneous addition of PPs from two consecutive bits using a novel approximate adder. The proposed multiplier is utilized in a mean filter structure and implemented in ISE Design Suite 14.7 using VHDL and synthesized on the Xilinx Spartan3-XC3S400 FPGA board. Compared to the literature, the proposed multiplier achieves power and power-delay product (PDP) improvements of 56.09% and 73.02%, respectively. The validity of the expressed multiplier is demonstrated through the mean filter system. Results show that it achieves power savings of 33.33%. Additionally, the proposed multiplier provides more accurate results than other approximate multipliers by expressing higher values of peak signal-to-noise ratio (PSNR), (30.58%), and structural similarity index metric (SSIM), (22.22%), while power consumption is in a low range.

cs.AR

Hermes: Unlocking Security Analysis of Cellular Network Protocols by Synthesizing Finite State Machines from Natural Language Specifications

In this paper, we present Hermes, an end-to-end framework to automatically generate formal representations from natural language cellular specifications. We first develop a neural constituency parser, NEUTREX, to process transition-relevant texts and extract transition components (i.e., states, conditions, and actions). We also design a domain-specific language to translate these transition components to logical formulas by leveraging dependency parse trees. Finally, we compile these logical formulas to generate transitions and create the formal model as finite state machines. To demonstrate the effectiveness of Hermes, we evaluate it on 4G NAS, 5G NAS, and 5G RRC specifications and obtain an overall accuracy of 81-87%, which is a substantial improvement over the state-of-the-art. Our security analysis of the extracted models uncovers 3 new vulnerabilities and identifies 19 previous attacks in 4G and 5G specifications, and 7 deviations in commercial 4G basebands.

cs.CR