index.html

---
title: Arcana
layout: default
---
			
<!-- Banner -->
	<section id="banner">
		<header>
			<h2>Map2Check: <em>Finding Software Vulnerabilities using Symbolic Execution and Fuzzing</em></h2>
			<a href="{{ site.baseurl }}/documentation.html" class="button">Learn More</a>			
		</header>
	</section>

<!-- Highlights -->
	<section class="wrapper style1">
		<div class="container">
			<div class="row double">
				<section class="4u">
					<div class="box highlight">
						<i class="icon major fa-paper-plane"></i>
						<h3>Automatic Test Generation</h3>
						<p style="text-align:justify">Map2Check is a method of automatically generating and 
						checking safety properties (e.g., Unreachability of Error Function, and Memory Safety) in C programs.</p>
					</div>
				</section>
				<section class="4u">
					<div class="box highlight">
						<i class="icon major fa-pencil"></i>
						<h3>Analysing C source code</h3>
						<p style="text-align:justify">Map2Check adopts source code instrumentation to monitor data 
						from the program’s executions, aiming to verify the generated test cases and to detect failures 
						originating from the safety properties of the analyzed program.</p>
					</div>
				</section>
				<section class="4u">
					<div class="box highlight">
						<i class="icon major fa-wrench"></i>
						<h3>Architecture, Implementation and Availability </h3>
						<p style="text-align:justify">Map2Check is implemented as a source-to-source transformation tool 
						adopting a collection of modular and reusable compiler and tool chain technologies, e.g., LLVM.</p>
					</div>
				</section>
			</div>
		</div>
	</section>

<!-- Gigantic Heading -->
	<section class="wrapper style2">
		<div class="container">
			<header class="major">
				<h2>Finding Software Vulnerabilities by Test-Case Generation of C Programs</h2>
				<p>Map2Check is a software verification tool to check for safety properties 
					about pointer safety, memory leaks, invalid deallocation, overflows, 
				    and unreachability of error location.</p>
			</header>
		</div>
	</section>

<!-- Posts -->
	<section class="wrapper style1">
		<div class="container">
			<div class="row">
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/LLVM-Logo-Derivative-4.png" alt="" /></a>
						<div class="inner">
							<h3>LLVM Compiler Infrastructure</h3>
							<p style="text-align:justify">In this new version of Map2Check tool, we have been 
							adopted <a href="http://llvm.org/">LLVM</a> as a compiler framework to improve our 
							code instrumentation and optimizations.</p>
						</div>
					</div>
				</section>
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/klee.png" alt="" /></a>
						<div class="inner">
							<h3>KLEE LLVM Execution Engine</h3>
							<p style="text-align:justify">Our tool adopts <a href="http://klee.github.io">KLEE</a> as 
							a symbolic execution engine that is capable of automatically generating tests that 
							achieve high coverage on a diverse set of complex programs.</p>
						</div>
					</div>
				</section>
			</div>
			
			<div class="row">
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/AFL_Logo.gif" alt="" /></a>
						<div class="inner">
							<h3>AFL FUzzer</h3>
							<p style="text-align:justify">Our tool adopts <a href="http://lcamtuf.coredump.cx/afl/">American 
							Fuzzy Lop</a> as a compile-time instrumentation and genetic algorithms to automatically discover 
							clean, interesting test cases that trigger new internal states in the targeted binary.</p>
						</div>
					</div>
				</section>
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/competition.jpg" alt="" /></a>
						<div class="inner">
							<h3>SV-COMP</h3>
							<p style="text-align:justify">Map2Check has been participed in the Intl. Competition on Software 
							Verification (<a href="https://sv-comp.sosy-lab.org">SV-COMP</a>) held at TACAS.</p>
						</div>
					</div>
				</section>
			</div>

			<div class="row">
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/metaSMT.png" 
							alt="Image from https://doi.org/10.1007/s10009-016-0426-1" /></a>
						<div class="inner">
							<h3>MetaSMT</h3>
							<p style="text-align:justify">Our tool adopts <a href="https://doi.org/10.1007/s10009-016-0426-1">
								MetaSMT</a> to improve our solvers supported. MetaSMT is a wrapper around various SMT or 
								SMT-like solvers. This means you are able to program against this library and use any of 
								the implemented solvers.</p>
						</div>
					</div>
				</section>
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/crab_llvm.png" alt="" /></a>
						<div class="inner">
							<h3>CRAB-LLVM</h3>
							<p style="text-align:justify">Our tool adopts <a href="https://github.com/seahorn/crab-llvm">Crab-LLVM</a> 
								is a static analyzer that computes inductive invariants for LLVM-based languages based 
								on the Crab library.
							</p>
						</div>
					</div>
				</section>
			</div>
			
			<div class="row">
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/pic03.jpg" alt="" /></a>
						<div class="inner">
							<h3>Searching for Contributions</h3>
							<p style="text-align:justify">We have new plans to keep improving Map2Check tool, but if you 
							have new ideas, please tell us.</p>
						</div>
					</div>
				</section>
				<section class="6u">
					<div class="box post">
						<a href="#" class="image left"><img src="{{ site.baseurl }}/assets/images/pic04.jpg" alt="" /></a>
						<div class="inner">
							<h3>Research</h3>
							<p style="text-align:justify">Map2Check tool have improved based on academic research, 
							more details checkout <a href="{{ site.baseurl }}/publications.html">Publications</a>.</p>
						</div>
					</div>
				</section>
			</div>
		</div>
	</section>