Event Start

About

The AFRiTS one-day Workshop, co-allocated with SBMF 2023 (Brazilian Symposium on Formal Methods), aims to bring together researchers working on challenges at the intersection between artificial intelligence (AI) and cyber-security, including security for AI and AI for security.

We are particularly interested in discussing recent achievements and future initiatives to address the fundamental security problem of guaranteeing safety, transparency, and robustness in neural-based architectures and their implementation in computer-based systems. Regarding safety and robustness, one important observation is that it is becoming more difficult to achieve these properties since fixed mathematical models are being replaced by machine learning (ML) approaches, where the future operation may change based on data acquired during previous actions due to model updating. Indeed, ML algorithms have a dual role in formal software verification development: "model evolution" and "verification enhancement", which we intend to discuss in AFRiTS.

We will have invited talks, poster presentations, an "Automated Formal Reasoning for Trustworthy AI Systems" roundtable discussion on how to make the formal verification process more automatic, whether using SAT, SMT, BMC, AR, and other reasoning technologies, to achieve safety, transparency, and robustness in learning-based systems.

Participants will leave having a better understanding of enabling system designers to specify essential conceptual/behavioral properties of neural-based systems, verify them, and thus safeguard the system against unpredictable behavior and attacks. Therefore, we will foster the dialogue between contemporary explainable neural models and full-stack neural software verification.


Areas of interest


Figure above illustrates the main research areas in automated formal reasoning for trustworthy AI systems we want to cover in this workshop. It covers methods, techniques, algorithms, and tools to detect, classify and repair security vulnerabilities in AI systems. Therefore, the workshop's primary goal is to establish new partnerships/collaborations to discuss the challenges at the intersection between AI and cyber-security: security for AI and AI for security and tackle our main obstacles to achieving widespread adoption of trusted and secure AI systems.

Preliminary Program

# 05/12/2023
9:00-10:00 Edoardo Manino

Title: A Tale of Two Oracles: Defining and Verifying when AI Systems are Safe

Slides: click here.
10:00-10:30 Jefferson Andrade

Title: Dynamic Epistemic Logic in Neural Layer Transparency: Towards a Formal Understanding of Knowledge Evolution in Neural Networks

Slides: click here.
10:30-11:30 Sérgio Campos

Title: Stochastic Formal Model of PI3K/mTOR Pathway in Alzheimer's Disease for Drug Repurposing: An Evaluation of Rapamycin, LY294002, and NVP-BEZ235

Slides: click here.
11:30-12:00 Edoardo Manino, Rafael Menezes, Fedor Shmarov and Lucas Cordeiro

Title: NeuroCodeBench: a plain C neural network benchmark for software verification

Slides: click here.
12:30-14:30 Lunch
14:30-16:30 Janislley Oliveira de Sousa

Title: Memory Safety in Linux Kernel Drivers: Enhancing Security with Formal Verification

Description:

The rapid evolution of software development has resulted in increasingly sophisticated systems. In the midst of this evolution, the Linux kernel, a cornerstone of many devices from servers to smartphones, stands out due to its open-source nature and wide adoption. However, this vast and intricate codebase, riddled with deep interdependencies, has also become a focal point of security concerns. It's no surprise given the kernel's pivotal role in mediating between hardware and software elements.

This workshop delves into the heart of ensuring memory safety within Linux kernel drivers. As the industry moves towards integrating Linux-based systems in vital sectors such as mobile systems, automobile control units, and even medical equipment, the emphasis on kernel security has never been higher. Traditional methods, including extensive testing and code reviews, though vital, often miss subtle bugs that can lead to catastrophic system failures and security breaches.

In the realm of formal verification, which offers a mathematically-backed approach to affirm program accuracy, various tools have surfaced. Among them, ESBMC stands out as particularly skilled in analyzing vast software systems. However, when faced with the intricate Linux kernel, characterized by its expansive code and deep directory dependencies, challenges inevitably arise. Enter LSVerifier, specifically designed for this landscape. This tool provides robust solutions to navigate and address the intricacies of the Linux kernel, ensuring a more comprehensive and precise analysis of its security nuances.

-->

Important Dates

September 1st September 15th Paper submission deadline
Ocotber 1st October 15th Acceptance notice
October 15th October 30th Camera-ready copy deadline
5th of December AFRiTS 2023

Registration

More information about fees and registration is available on the SBMF2023 website.

Committees

Organizing Committee:

Organizers

Program Committee

Submission instructions

We invite researchers to submit an extended abstract (at most 4 pages) describing the research they intend to present in the workshop. These abstracts will be peer-reviewed and published at https://ceur-ws.org.

Abstracts should present unpublished and original work that has a clear contribution to the state-of-the-art on the theory and practice of formal methods.

Submissions should be made via this link: https://easychair.org/conferences/?conf=afrits2023

Manaus

Manaus, located on the banks of the Negro River in northwestern Brazil, is in the heart of the world's largest rainforest and is one of the biggest tourist destinations in Brazil. It is also the main financial, corporate, industrial, research, technology, entertainment, and commercial center of the Northern Region of Brazil. The city is situated at the confluence of the Negro and Solimões rivers, with the Teatro Amazonas listed as a National Historic Heritage by IPHAN its greatest cultural symbol.
Manaus was home to the first higher education institution in Brazil, founded on January 17, 1909. This originated from the defunct Free University of Manáos, which dismembered the Faculty of Law, forming the embryo of the current UFAM.
The Institute of Computing of the UFAM, which has only 30 years of history, is one of the two most important centers of higher education and research and entrepreneurship in computing startups in the North and Northeast of Brazil, being recognised as a postgraduate program of international level according to the most recent ranking by Capes, an agency of the Ministry of Education that promotes research and graduate studies.

Teatro Amazonas

The main cultural and architectural symbol of the state, Teatro Amazonas, located in Largo de São Sebastião in the heart of Manaus, keeps alive much of the history of the rubber boom, the golden age of the Amazonian capital. Inaugurated on December 31, 1896, the theater surprises and delights with its grandeur.

The concert hall seats 701 people, spread between the audience and three floors of boxes. It's impossible not to be mesmerized by the concave ceiling, which features four canvases painted in Paris by the renowned Casa Carpezot. The canvases depict music, dance, tragedy, and opera. In the center hangs a majestic French bronze chandelier. The masks on the columns of the audience, which pay tribute to composers and playwrights, are also noteworthy.

The Teatro Amazonas' boca cloth is another rarity. It was created in 1894 by Brazilian artist Crispim do Amaral and depicts the confluence of the Negro and Solimões rivers.

Nowadays, the theater hosts major events organized by the State Secretariat for Culture and Creative Economy, such as the Amazonas Opera Festival and the Dance and Theater festivals; high-brow performances like those presented by the State's Artistic and Cultural Bodies; and popular shows that benefit local artists of all genres.. More information (in portugues only) can be seen here.


Provincial Palace (Palacete Provincial)

The Provincial Palace houses three museums of different kinds: the Museum of Image and Sound (MISAM), the Museum of Numismatics of Amazonas, the Tiradentes Museum, the Pinacoteca do Estado, and the Archaeology Exhibition.

The building was founded in 1874 and served as the headquarters of the Military Police of Amazonas for more than 100 years. On March 24, 2005, it was transformed into a restaurant. However, it was reopened in 2009 as a museum, and the space is now open to the public free of charge. Visitors can come to learn about the collections and art of the museums, and the space also hosts cultural events that attract children, young people, and adults. Heliodoro Balbi Square (formerly Police Square), in front of the building, is an extension of the tour to the site.

The Pinacoteca has paintings, photos, and engravings by local, national, and international artists. The Museum of Numismatics has a collection of over 35,000 pieces and ancient coins. MISAM has DVDs and CDs that can be viewed for free on site. The Tiradentes Museum honors firefighters and state police, and exhibits weapons and uniforms. The Archaeology Exhibition reproduces excavations and artifacts discovered in the region.

Click here for more information

Event Location

The IComp, the venue of the 26th SBMF and the AFRiTS, is located on the UFAM Campus, which covers an area of about 600 hectares. The campus is home to a variety of ecosystems, including native and secondary forests, plateaus and floodplains, meadows, and deforested areas with plantations. The campus is located on the east side of Manaus and is surrounded by neighborhoods and avenues.

Host and co-host organizers



Sponsorship