Sen, AmartyaWakam Younang, Victorine ClotildeFu, HuirongRaj, SunnyDrignei, Dorin2026-07-172026-07-172026-01-01https://hdl.handle.net/10323/22139The widespread adoption of Internet of Things (IoT) devices and Autonomous Vehicles (AVs) has created a significant assurance gap between what users expect and what is technically feasible in resource-limited environments. As these systems transition from prototypes to critical infrastructure, it becomes essential not only to make them efficient, but also to ensure they are demonstrably secure and capable of earning public trust. This dissertation introduces a multi-layered research framework that tackles this gap across four stages of the technology lifecycle: socio-technical, operational, security-evaluative, and formal-foundational.The first phase situates the problem by examining the disconnect between governmental policies and end-user priorities related to AV safety and privacy. After identifying that public trust is frequently weakened by opaque automated decision-making, the work moves in the second phase, which focuses on security, especially assessing security risk in IoT networks, by leveraging complex numbers Bayesian Attack Graphs to model and quantify unpredictable attacker behavior. Once the risk can be assessed, the most common step is to mitigate the risk. The work focuses on assessing how realistically security models can be deployed on edge devices, especially Intrusion Detection Systems (IDS) models, on vehicles CAN buses, introducing new feasibility metrics, that account for the IDS models accuracy, as well as the CAN bus resources restrictions. The final phase directly addresses the core of the security assurance gap by connecting imperative software implementations to rigorous mathematical proofs. It introduces the Tiered Isomorphic Alignment (TIA) framework, which helps automate the translation of Python programs into Isabelle/HOL formal specifications, and introduces CryptoGraph, a neuro-symbolic system that employs Graph Attention Networks to analyze the security of non-standard lightweight cryptographic ciphers. Taken together, these contributions establish a scalable, end-to-end methodology for designing the next generation of IoT ecosystems, one that is grounded in mathematical correctness and automated security assessment, capable of maintaining and enhancing public trust.CybersecurityFormal methodsGenerative AINeuro-symbolic AIRisk assessmentTrustworthy AI