Ellen Tsaprailis, May 9, 2022
Photo credit: Lindsay Ralph
Ericsson Fellow and Grad Student James Baak has a Passion for Formal Methods
James Baak is one of six graduate students who are Ericsson Fellows at Carleton University—a unique, talent-building program born out of the Ericsson-Carleton University Partnership for Research and Leadership in Wireless Networks.
Instead of working as a teaching assistant during their graduate studies, Baak and the other fellows are being supported to fully focus on their pioneering wireless communications research and get input from both their academic supervisors and Ericsson professionals.
For Baak, his research specialty is diving into automating formal methods.
“I want to bridge the gap between the average designer/developer and have an automated process to introduce them to formal methods,” says Baak of his long-term research goal.
Baak has a Bachelor of Engineering from Carleton, and during his undergrad did a series of co-ops that included government and private industry which provided him relevant work experience and an initial plan to pursue employment after graduating.
His academic trajectory took a turn when Baak registered for a security engineering course run by Systems and Computer Engineering Assistant Professor Jason Jaskolka in his final year.
“Without the intention of going to my master’s, Professor Jaskolka and I aligned on some of our views of the use of formal methods in computer systems engineering,” says Baak. “I was quite interested in defining a fully-automated process or formal method to use mathematics or other rigorous notation methods to define, verify and validate systems.”
Soon after, Baak was invited to start working in Carleton’s Cyber Security Evaluation and Assurance (CyberSEA) Research Lab run by Jaskolka who also agreed to be Baak’s academic supervisor for his fellowship.
“James is a valued member of the CyberSEA Research Lab and it’s a pleasure to supervise his research,” says Jaskolka. “James is developing an approach for reusing formally verified components to address security concerns in the design and development of 5G systems. Through engagement opportunities offered by the Ericsson Fellowship, James has been able to understand the real needs of Ericsson so that his work can be applied in practice. James’ progress to-date has been met with interest by Ericsson, specifically in its potential to help reduce the time and effort required to design and verify critical systems and networks.”
Using the Alloy language system, Baak is applying his idea of compositional component-based design to ensure safety in 5G systems.
“When we think of components in software engineering, it’s kind of like this independently deployable piece of code that you can put anywhere. What I’m interested in is bringing those components together and connecting them in a way that we can divide and conquer the verification process,” explains Baak.
“Usually in the types of systems using formal methods it is a mathematical notation of all these components brought together, but it is large and when we give it to a computer or even a human to analyze, it becomes very difficult and complex to go through it and verify that the system is functioning the way it should. So, the goal with my research is to be able to divide up the verification process by defining abstract boundaries around groups of components.”
Breaking up the verification process into groupings instead of the whole system would be faster and easier to keep components secure.
“For example, a web browser client and website server are two separate components of a distributed system which communicate with each other to provide a service to a client,” explains Baak. “The web browser and the server can be further broken down into their sub-component groups to provide the different functionality of the client or server. The verification of the components can then be verified individually or in their groups. Logically, we should be able to say these things can be developed and verified independently as long as certain assumptions and constraints are held true between components when we connect them.”
An Ericsson Fellow since Sept. 2020, Baak is in his second year of a master’s of applied science in electrical and computer engineering degree and plans to graduate this summer. Throughout this second year, Baak has been able to devote all his time to his thesis and 5G research.
Baak’s goal after completing his master’s is to pursue employment in the private sector, perhaps with Ericsson, and is hoping to continue this particular research.
“I’m quite interested in this type of methodology,” says Baak. “I would be very interested to try implementing it in the actual industry. It’s very easy to talk about in academia and show some examples on smaller systems, but it’s another thing to actually go into the industry and apply it.”
Ericsson Fellowship
In this prestigious fellowship program, Carleton graduate students conduct hands-on research alongside Ericsson experts in state-of-the-art facilities, ensuring students build skills that are in high demand in today’s telecommunications industry.
Share: Twitter, Facebook