WebAssembly är ett nytt lågnivåspråk vilket fungerar som kompileringsmål och körs i webbläsare. Allt eftersom att mer programkod körs på klientsidan av webbprogram har säkerheten av dessa program blivit mer viktig. Vårt arbete nyttjar formella verifikationsmetoder för att bevisa att ett program uppfyller en eller flera säkerhetsegenskaper. Mer specifikt har vi i denna avhandling utforskat användandet av relationssymbolisk exekvering i syfte att utföra formell verifiering av säkerhetsegenskaper för WebAssemblyprogram. Vi har beskrivit en formell semantik för relationssymbolisk exekvering för WebAssembly, implementerat det i Redexramverket, utökat implementationen för verifiering av konstanttidssäkerhet samt använde implementationen för att formellt verifiera flera urval av program, inkluderande Salsa20. Vårt arbete visar att relationell verifiering av standardsäkerhetsegenskaper såsom icke-interferens samt konstanttidssäkerhet är genomförbart via relationssymbolisk exekvering för WebAssembly är genomförbart.