The Frama-C Software Analysis Platform

Blog Post by: Kaitlyn Khan, Hamza Rashid, Tom Reingold, Tong Chen        

        I personally have never heard of Frama-C before, but I am impressed by all of the applications and abilities this program has to offer. Many coding platforms such as Visual Studio Code already implement
debuggers that will notify the user of a missing element or undeclared variable. These are some examples of how programs adapted to become smarter and self-replicating. I wanted to write about how Frama-C is outlining the potential in artificial intelligence based applications. The article already describes the benefits of Frama-C as a tool to parse code and verify software for reputable organizations such as Mitsubishi and NASA. Since even tests with over 80,000 lines of code can successfully be covered within 8 hours and output 86% of function, the numbers prove its validation. (KK)

        Frama-C paves the way for machine learning and makes understanding algorithms an easier task for those studying in computer science. This may be why more and more countries are implementing this software in their lectures. I wonder if CUNY will be implementing this soon for beginner programmers. Using abstract interpretation techniques to static verify code helps users learn from their mistakes and ultimately limits runtime errors. Even the annotations can be compiled and executed, which I find to be the most sublime. I am curious how much further Frama-C could be developed, or even referenced to create a similar platform for other coding languages. As AI continues to advance, less jobs in the computer science field become replaced by automatons. How long until programs are able to write its own code and fix bugs within the need for human intervention? These are some of the questions that transpire after reading about the advancements in software engineering. (KK)

One of the plugins mentioned that stood out to me was Eva which uses abstract interpretation. The plugin will try to anticipate possible values for variables. Eva will use abstractions and over approximate. (HR)

In the example figure 4a, the function expects a character to be entered. In the first case, if the character is a *, both x and y are set to 0 otherwise both x and y are set to 1. On line 11 sum = x + y, and on line 14 res = 10/sum. In this example, if a * is entered sum will equal 0+0, and res will = 10/0. Eva will be able to detect this division by 0 by using the over approximations. On the line with sum = x + y, Eva over approximates the possible values for the sum variable as {0,1,2}. In this case, only 0 and 2 are possible values for sum. (HR)

In figure 2b, in both cases the sum will equal 1, but Eva will still over approximate the possible values for sum as {0,1,2}, and report a false alarm. This would be a major problem for users. To prevent this Eva can divide the possible paths and analyze them separately. The possible values will be {1}. However, getting the more precise results will increase processing time. In my opinion this type of anticipation is very useful in the real world. While someone is writing code the errors will be reported so the problems can be solved faster than with manual analysis. While there are still flaws with the method, I see a lot of potential with this plugin. (HR)

Frama-C can be very useful for a programmer inheriting code that someone else has written, especially if the original author is not available. I was once tasked with taking over a departed employee's code and owning it as my own. My job was to fix bugs and enhance the software. It took me a long time to understand the code, and perhaps Frama-C could have helped. (TR)

I also think Frama-C would be good in a collaborative environment to ensure that programmers follow the organization's published style guide. Producing modular code is much easier when all code is written in the same style. (TR) 

Frama-C contains several plugins each with a unique and useful feature. The following is a list of some of them ACSL, Eva, WP, E-ACSL, Path-Crawler, Aoraï, CaFE, RPP, MetASCL, Conc2Seq, LAnnotate, StaDy, LUncov, Slicing, SecureFlow. (TC)

The ACSL plugin has clauses that can be anywhere in the code for the purpose of function contracts, keeping track of bits of the functions, and providing more details on parts of the function. Function contract is the precondition that the function may be called and the information that it may return as the function ends. (TC)

The Eva plugin analyzes the code and prevents and provides feedback on undefined behaviors such as invalid memory access, uninitialized memory read, division by zero, signed inter overflow, undefine bit shift, invalid pointer comparison. It is in charge of the syntax and correctness of the code. (TC)

The WP plugin scans the code and keeps tracts of the states of the code to make sure that the conditions for the code are respected. It basically allows the code to work in the way how the coder intended. (TC)

The E-ACSL plugin verifies and checks the specifications implemented when the code is run. (TC)

The Path-Crawler plugin generates a test for the code that allows the user to check if the code is working as how he/she is intending it to work. It is useful for making sure that there aren’t special cases where the function would fail to work as intended. (TC)

The Aoraï and CaFE plugin allows guides the functions to be executed in the correct order. It has states that changes as functions are being executed to allow the execution to end in the correct place. (TC)

Comments

Post a Comment

Popular posts from this blog

Our first class

Image
  We had our first class today. Hamza, Katie, Tom, and Tong agreed to be in group 3. This blog is named atomizeGothamtank because it is an anagram of our names, and we live in Gotham City. (Tom) We discussed what we might like the project to be. We're not sure. Maybe a game. Maybe something that processes data such as a class registration system. (Tom) We discussed platforms. We took inventory of the group's computing facilities. We thought perhaps we could develop an iOS game, but that requires Xcode. Xcode requires a Mac, and not everyone has one. Maybe that's OK because not everyone needs to work on the iOS portion. Those without Macs could do the backend work. Tom offered to share his Mac with the others remotely, but it remains to be seen if that's viable. (Tom) We envisioned a client-server app that runs on the web. Perhaps it would render properly on both a mobile browser and a computer browser. The back end (webserver) would be on a Linux system because Tom offe...
Read more

Final Report

  CSCI 499 Final Report By: Hamza Rashid, Kaitlyn Khan, Tom Reingold, Tong Chen Hamza Rashid My contribution to the project is the streamplayer website. The code reads from a csv, user1.csv, which is a users 8 selected “favorite” radio stations. My code fetches the csv and then processes the data, loading 8 divisions which would contain the stream, as well as a play/pause button. Once this is loaded the user is presented with multiple options, such as being able to change the 8 available “favorite” streams. To make this easier for users, the available radio stations are loaded into a drop down menu. Simply select the radio stream number, the station you would like to select, then hit change. If it is successful an alert will appear on screen. Finally users have an option to save the new “favorite” streams. Hitting save will update the user1.csv in the server, an alert will appear if it was successful. (Hamza Rashid) To organize my code I broke up parts of my code into functions. ...
Read more

A Unified Theory of Garbage Collection

  Blog Post by: Kaitlyn Khan, Hamza Rashid, Tom Reingold, Tong Chen Tracing garbage collection and reference counting have many parallels. Tracing starts at the roots and aims to find the live data. Reference counting starts from anti-roots, which are the objects whose reference counts are zero, and aims to find the dead data. In this sense reference counting is the complement of tracing. Tracing starts from a count of zero, and increments to the true count. Reference counting starts with an excessive count and decrements to the true count.(HR)  As mentioned above, tracing will initialize the count to zero. A work-list, which is the set of objects to be processed, is used in the algorithm. While iterating through the list, if a new vertex is encountered, all of it's outer edges will be added to the work-list. Once the loop is finished all the live nodes will be discovered. A separate function is used to return the unused nodes to free the storage.(HR)  Reference cou...
Read more