Master Thesis, 30 hp: Integrate a packet-switching traffic manager block with HOL4P4

Master Thesis, 30 hp: Master Thesis: Integrate a packet-switching traffic manager block with HOL4P4Are you a student eager to apply your theoretical knowledge and fresh perspectives to real-world challenges? At Saab, we believe that innovation thrives on new ideas, and your master thesis project could be the spark that ignites our next technological breakthrough. Your roleWe recognize the immense value that students bring to our company. Your academic rigor, combined with your enthusiasm for cutting-edge technology, allows you to approach problems with a unique and insightful lens. At Saab, you'll have the opportunity to collaborate with experienced engineers and specialists, gaining invaluable practical experience while making a tangible contribution to our growth and development. BackgroundIn network switch devices, the traffic manager (“TM”) is a component that handles internal packet buffering, along with scheduling, drop policies and replication. Specifically, in the context of P4-programmable data planes, the TM is in most architectures located between the ingress and egress stages of data plane processing. The ingress stage sets egress port, or multicast group for a packet, and the TM must then direct and prioritize traffic.Description of the Thesis ProjectThe goal of this Master’s degree project is to implement a TM in the CakeML and/or Pancake languages and then integrate it with the programmable software switch HOL4P4.EXE, which is based on a formalization of the P4 language in the interactive theorem prover HOL4. The TM should be a separate binary that interfaces with the ingress and egress parts via Unix raw sockets or other similar mechanism. Accordingly, optimally utilizing CPU architectures with multiple cores is also an objective. The result should then be validated by an extensive test suite, to ensure compliance with e.g. the IEEE 802.1Q standards it implements.More advanced TM functionality that may be explored if time allows includes prioritization based on QoS and evaluation of different scheduling algorithms (strict priority, deficit round-robin). In addition, demonstrating support for different architectures (for example, ARM and RISC-V are both supported by the existing toolchain) and comparatively benchmarking the result on real multicore hardware (for example, Raspberry Pi 5) would be interesting. The overarching end goal to which this project contributes is to enable a fully-featured, formally verified software switch. Note that while this project is based on a toolchain involving interactive theorem provers, it does not require any experience in interactive theorem proving.Your profileThe project is suitable for one student in the final stage of a Computer Science degree programme, who is about to begin a 30 hp thesis project. You are studying Computer Science with a specialization in Software Engineering and Management, a programme that combines traditional software and systems development with testing methodologies and agile project management. Strong emphasis is placed on project-based learning and practical experience. Knowledge of the P4 programming language and demonstrated hands-on experience working with it are required. Geographical proximity to our operations in Linköping or Lindholmen is highly desirable. Applicant requirements for this thesis:Intermediate level of P4 programmingUnderstanding of the data plane implementation of common network protocolsGeneral knowledge about switch and router hardware We provide the support and guidance you need to translate your theoretical knowledge into practical solutions. Join us and become a driving force behind Saab's technological advancements!This position requires that you pass a security vetting based on the current regulations around/of security protection. For positions requiring security clearance additional obligations on citizenship may apply.Kindly observe that this is an ongoing recruitment process and that the position might be filled before the closing date of the advertisement.Contact informationPatrik Johansson, Managerpatrik.pj.johansson@saabgroup.com What you will be a part ofExplore a wealth of possibilities. Take on challenges, create smart inventions, and grow beyond. This is a place for curious minds, brave pioneers, and everyone in between. Together, we achieve the extraordinary, each bringing our unique perspectives. Your part matters. Saab is a leading defense and security company with an enduring purpose, to help nations keep their people and society safe. Empowered by its 28,000 talented people, Saab constantly pushes the boundaries of technology to create a safer and more sustainable world. Saab designs, manufactures and maintains advanced systems in aeronautics, weapons, command and control, sensors and underwater systems. Saab is headquartered in Sweden. It has major operations all over the world and is part of the domestic defense capability of several nations. Read more about us here.