We will explore the use of LLMs (Large Language Models) in conjunction with formal methods. Our work will focus on safety critical programs written in the programming language Rust for which we will use finetuned LLMs to audit Rust programs and assist in formal verification of cryptographic code and other security critical applications. Concretely, the project will proceed in two tracks: 1. Exploration of an AI powered automatic code reviewer, focusing on security and vulnerability checking. 2. Translation of security specifications in natural language into formal specifications using LLMs for the verification of Rust code
-
175000
DKK
Anders Laustsen,
CenSec hovedkontor
Gravene 2, 1. th.
8800 Viborg
CVR: 30629809
CenSec København
Bredgade 35D
1260 København K
CenSec Aarhus
Erhvervshus Midtjylland
Åbogade 15
8200 Aarhus N
CenSec Vojens
Erhvervshus Sydjylland
Billundvej 3
6500 Vojens