Innovating Web Security: Formal Verification and Automated Analysis for WebAssembly

Innovating Web Security: Formal Verification and Automated Analysis for WebAssembly

Presenter(s)

Viet Viet Bui

Comments

Presentation: 1:00-1:20, LTC Studio

Description

In the realm of web security, escalating data leakages cause substantial financial losses, surpassing hundreds of millions annually. Traditional security measures, while necessary, have shown their limitations, as evidenced by the relentless succession of cyberattacks. These vulnerabilities largely stem from human-generated errors in coding, among other critical oversights, highlighting an urgent need for a more reliable and robust security approach.Our primary goal is to transform web security through the strategic application of formal methods and WebAssembly. This initiative is structured with three specific aims. Firstly, our approach utilizes formal verification tools like the Coq Proof Assistant to enhance code integrity and mitigate initial vulnerabilities in WebAssembly programming. Second, we aim to bolster the protection of user-specific data, such as cookies, by seamlessly translating WebAssembly programs into the Coq environment for thorough formal analysis, thus providing a formidable defense against widespread cyber threats. Third, through a compilation of benchmarks and case studies, we strive to set new benchmarks in web security standards using formal verification. Our mission is to dramatically reduce both the frequency and severity of cyber-attacks, showcasing our methodology's capability to foster a more secure digital environment.

Publication Date

4-17-2024

Project Designation

Graduate Research

Primary Advisor

Luan V. Nguyen, Phu Huu Phung

Primary Advisor's Department

Computer Science

Keywords

Stander Symposium, College of Arts and Sciences

Innovating Web Security: Formal Verification and Automated Analysis for WebAssembly

Share

COinS