Coming up next, we've got a talk on Ada, exploitation in the era of formal verification, a peek at a new frontier with AdaCoreSpark. So please help me welcome to the stage Alex and Adam. Hello everyone, and welcome to the presentation in the exploitation in the era of formal verification. A peek at the new frontier with AdaCoreSpark. Some folks already approached us and asked what is this picture here. You can see the answer is pretty dumb because there is no logic behind that. It's just kind of visualization that in any kind of software you might have a wrong path, correct path, failed path, and some of the path could be correctly verified. Some of the path is just wrong or undefined behavior. This picture looks cool. That's why we decided to use it, but don't find any meanings here because there is not. If you find, let me know. I'll be happy to listen.  My name is Adam, and together with Alex, we have been doing some security research for some time already for a few decades to be honest. And yeah, there is some private contact to us, some short bio to us. And this research has been done during our work at NVIDIA. Both of us work at NVIDIA currently. So yes, apparently this research which we are going to present is not only the results of our work, but entire offensive security research team, which I'm currently leading. And Big Kudos also to Jared, Max, and Nikola, which also are involved in this research. And before we also move to the formal verification problem, especially in the software, we need to speak a bit more about software vulnerabilities, because this is what the formal verified method is supposed to address. And you cannot speak about the software vulnerabilities without touching the problem of memory safety. So just a quick intro about memory safety. What is memory safety? It's apparently a term used by security engineers to describe a state of being protected from various bugs related to memory access. And of course, there's a bunch of bugs who falls into this category, including every type of overflow, some memory, like on the stack, on the heap, on the global, every piece of the memory which can be overflowed, any kind of out-of-bump, read and write. And invite page, including null portable reference, any kind of use after free, use after return, use after scope, etc. There's many types of use after bugs. Also, any type of untilized memory, including wild pointers or memory leaks, invite free. All of that, it's a memory safety issue. But not all of the security vulnerabilities are memory safety issues. So some of them, like any type of the overflows, integer overflows, arithmetic overflows are not memory safety issues. Logical issues is also not memory safety issue. Error handling race condition, there's a star, because race condition on data access is type of the memory safety issue, but in general, it's not. And there's a few more. But what is worth to mention that even this is not a memory safety issue, they often result in memory safety issues. So if you have any kind of integer overflow on the size of how much data you want to copy, it's not memory safety issues, but when it starts to copy the data, then you will have a memory safety issue. So why we even speak about memory safety? Because apparently memory safety errors are today the biggest attack surface. And I really mean it. It's the biggest software type of the bugs. And there's a few reasons behind that. Some of them are easy to spot, like this one. Memory unsafe language has been chosen to develop a core of the execution environment. So every type of the operating system like Windows, Linux, Macintosh are written in memory unsafe language, like CRC++. And the question is why? Because at that time, when this ecosystem has been developed, we already have memory safe language, which could give us opportunity to not have these bugs. But we still develop them in the memory safe language. There's a few reasons behind that. Some of them is because at that time, the hardware was not performed as well as today. That was much slower. And the code in the memory unsafe language was faster. And also it gives developers for fun growing control over the memory address where their code can be executed with the attributes. This is one of the reasons why memory safe was chosen to develop these ecosystems. Also memory safety bugs are very well researched, as everybody knows. Some professional exploiters even developed the exploitation framework to target exploiting software stack. I've seen by myself, reverse engineer, it's one of the framework developed to exploit Windows kernel vulnerabilities. You have a full framework. You just find the bug and expose primitive like read write and include into the framework and entire exploitation process magically runs. It bypasses a salar, bypasses any other mitigation. So you just find the bug, plug in the framework, run and it's done. So it's a very well researched idea. And additionally, memory researchers do automation on focusing for memory safety bug detection. They don't even need to understand what the software does. You just take an open source project. You recompile this with the various code coverage instrumentation.  And apparently it's kind of not rare that some researchers, they just pick up most popular libraries without going into detail to analyze what's the architecture it is. Let's just fuzz it. Let's find the bug and we have benefits, yes. So it's not also a theory because a big corporation starting to struggle with this problem more and more and they cannot ignore it anymore and they want to study a few cases and the biggest corporation who produced software is apparently Microsoft. And they also face this problem for ages and they make a few presentation about that which I want to recap here. So in 2002 Microsoft created something called Trustworthy Computing, TWC, where they wanted to, they cannot ignore any more the security issues in their ecosystem because larger customers like government agencies, financial companies starting to be impacted by the security problems on the windows and this is Microsoft products, and they need to ignore it and they needed to do something on that. So they created TWC and they focus on the few areas and one of them was security and as a pillar of this initiative and they developed as a direct implication of that, a few interesting things like TWC developed as DLC, security development life cycles process to be able to make the quality of the code higher from the beginning. They also created MSRC, which is Microsoft Security Response Center, which treated security bugs differently than any other bugs. So they also know that this is something which can impact the security of the ecosystem, so they are also starting to fuzz by themselves some of the software, they are also starting to do bug hunting, they are also starting to do exploit research, so they do a lot of interesting stuff and traditionally in 2019 they said, okay, we spent so much engineered effort, we spent so much money on that, do we see improvements? Do we see any benefits of all of that? In 2019 they analyzed the last 12 years of all of the security cases reported to them and that's what they saw. So this is slide from Microsoft itself. As you can see, the type of the security bugs which are reported to them are more or less the same over the time. In the 2006 around 70% of all of the security issues was memory safety issues and in 2018 we still see 70% of memory safety issues. So does it mean nothing changes over the time? Even of this years of investment? It's not obviously because this slide shows what changes. So we see that the type of the memory safety issues which are reported are differently. So in the beginning in 2006 we see the quarter of the bugs are stuck overflowing vulnerabilities while in the 2014 there is almost zero of them. And the reason is not because this bug disappeared, it just doesn't give benefits for the attacker because the modern mitigation makes the exploitation of this bug sometimes impossible or very hard. But in the same time they saw the rise of other type of issues like use after free, this is this gray box here. You can see the huge rise of them because there's no any mitigations on that so it's much trivial to exploit and then they introduce mitigation and you can see that the amount of the bugs are shrinking. And now we can see there is a rise on the edge of this year. You can see the rise of yellow which is type of the confusion because there is no mitigation so people move to that type of attack. So something changes but overall 70% of the bugs are memory safety issues. And Google case, let's speak about that because it's slightly different. They wanted to avoid the problem with Microsoft hats instead of patching bad software with adding new security layers. They wanted to make something differently. So they designed Google Chrome in the security in mind. They have a high code quality. They constantly fasted since 2015 because they knew the bugs will be there. They wanted to catch them in-house as soon as possible and you know Google has power. So they fuzz it in the various platform. They use OSS fast platform. They use Google Cloud platform which essentially means they have essentially unlimited computer power. They also have dedicated team to improve various mitigations and in 2020 they did exactly the same job. They analyzed all of the security issues since 2015 when they started to fuzz what were reported to them with the high and critical severity and guess what happened. They end up in exactly the same place. Even they took different approach. Roughly 70% of the bugs are memory safety issues. And half of these bugs are use after free bugs. And even more they knew that these bugs will be there. So they designed the Google Chrome in such a case that these bugs will be there, they knew this. They heavily sandboxed them and they make a warranty that one of the bugs is not enough to take over of the hots machine although this is a quote from their blog but we are reaching the limits of sandboxing and site isolation. And yeah, that's pretty concerning. And what about open source world? This open source world is different than corporation world. And there is not many research in this area although we found one interesting research done by Technical University in Darmstadt in Germany, Continental AG and Intel Labs which summarized it as we find no clear evidence that the vulnerability rate of widely used software decreases over the time even in the popular stable releases. The fixings of the bugs does not seem to reduce the rate of the newly identified vulnerabilities. So it's not much better I guess. So are we doomed? Is memory safety something who will be with us forever that we cannot fix anything? So apparently no. People trying to approach this problem because we understand it much more and we have a various ways how to try to address that. We have a new mitigation push to the hardware like memory tagging who are physically in the hardware trying to stop the memory safety issues from being exploited or even happens before it happens at first time. That's the memory tagging idea. We also have ideas of creating a new architecture of the memory like Cherry architecture. Cherry architecture treats differently in memory so it also will be redesigned the hardware. And there is a different approach, different path. Let's rewrite all of our software in the formally verified languages or use the language which has static method of proving that the memory safety doesn't exist. And people starting to rewrite the program in the Rust. But we have also the formal methods which is even stronger, which can formally prove that there is absence of memory safety issues and there is absence of undefined behavior. So pass form of verification you must be safe. And one of the language which is the most advanced of giving the attributes of the formal verified software is apparently at the course park where Alex will speak more about now. Yeah, let's read just a few key points from our presentation last year. Spark is a subset of other core language. It's basically a programming language formally defined including a set of analysis tools. And the real strength of this comes from these analysis tools. These are Gnat Proof, Gnat Stack and a few more. So one of the key features is that it's statically provable and the Proof is produced by this Gnat Proof tool. So you have to run it after you compile and build your code. So what can you achieve with this formal proof? So this tool can prove... Using this formal verifier you can prove that certain dynamic checks cannot fail. So you can just omit them. The compiler may omit them and do not build. That may give you some performance benefits. Also it can prove that there may not be run time errors. So everything runs in a well-defined state. You will not have any errors that raise in run time. And you will have hard proofs, like formal verifier. So also AIDACore Spark is memory safe language like Rust. But it also has a very strong typing system which is much stronger than Rust. So for example you will not have automatic overflow, integer overflow or stuff like that. And because of this it traditionally is used in industries such as automotive, IoT. Spark is safety certified. So NVIDIA constantly used that for build safety certified code. So the key points is that you can build buggy code but the problems are detected by the tools you really have to run them to actually verify that your code doesn't have any problems. And tools are orthogonal to each other. You have to run all of these tools because they detect different kinds of problems. So we approached the project written in Spark. We thought about this attack surface that we can use. So obviously no memory corruption bugs are there anymore because it is memory safety language. So also there are no pointers. So problems with pointers do not apply to Spark. But since 2019 Spark has a feature. So it's introduced the concept of pointers pretty much like Rust Borrow checking. So what about arithmetic security? So we have a very strong typing system so that's why arithmetic issues also don't apply. Our project was single threaded so we didn't care about parallel execution but if you do care about it there is extension to Spark called Revenskar which we can use. So what is left is attack surface. These are logic bugs and bad design. Obviously if you prove wrong things you can have correct proofs about wrong assumptions and you will have bugs in this case. Yes, so everything what Alex said it's compelling, sounds compelling. Apparently in Sery Cup you can have a buggy code you just must run all of the tools. If you don't run them you still have bugs. And the tools are orthogonal to itself so you must run all of them. If you don't speak some of them you will not have all of these benefits and most of the potential security issues must be in the design issues or in the logical errors. And bugs also can be introduced by the compiler itself which we can see later on the slides. So everything sounds very compelling and pretty interesting but benefits. Do we really see benefits in the software within Spark or any formal verified language compared to non-Spark code and apparently before we go there I just want to quickly say that what our team does because we did this evaluation so just to give you overview why we think we are the good guys to do this comparison we essentially work as a third party company inside of the company we just take a product after they pass all of the checkbox and they said okay ship it it's secure then we said no don't ship it let's review something which is the most critical it can import components so that's what we do and since 2020 we analyzed 17 very high product impact product which it's not a small feature it's a huge product and 10 of them used the software written in memory and safe language and 4 of them had the software written in Spark and what is important that 4 of this project was fully written in Spark there was not even single line of code written in the non-formally verified language and 2 of them was written in Spark and the Spark was the like imposer and enforcer of the security warranties of the software while inside they could be still software written in the memory and safe language but they didn't change the security warranties of the entire ecosystem so it's fine to have it there so we get a closer look on them and we wanted to compare do we really see the benefits and so first question how do we compare them how do you compare them as Apple to Apple not Apple to anything else and have some kind of bad impression about the quality of that so it's difficult so what we did we just we just put the raw data of all of the project which we reviewed we choose the one which could be compared we sort them out by the time frame of the review which we spent analyzing the software we also put what is the total back counts what is the percentage of the memory safety issue and what is the type of the software which we review and by sorting by the type we could be able somehow to compare because if the type of the software is the same we can more or less compare how do they behave with the formal verified language so first project in Spark could be also not could does not apply to this comparison because it's focused on the hardware modeling and we have nothing in the memory unsafe language to compare with so it was out of scope so we left with the free project in Spark which we can compare so let's look at the first one this is operating system like software which we fully develop in Spark and also we have in the memory unsafe language another type of the software also internally developed which was developed in C and C++ and as you can see we spent three weeks in the memory unsafe language for the reviewing and six weeks which is twice as long on Spark but we found only five ten bucks in Spark while we spent twice as long as reviewing the memory unsafe language and in the memory unsafe language we found 45 total back counts it's a huge difference as you can see there is almost 52% of the bucks 53% of the bucks are memory safety issues in the memory safe language while in Spark it's zero another software which is also good to compare is the project 4 the last project in the Spark which is a boot software also written in Spark and we spent almost the same amount of the time of reviewing as booting software in the memory unsafe language and apparently memory safe language boot software was not written by us, not written by NVIDIA it was written by external company although it was using NVIDIA products so that's why we reviewed it and as you can see we found around five bucks in the Spark and 17 bucks in the memory safe language again huge difference if you look at the percentage of the memory safety it matches the industry standard 65% are memory safety issue in memory safe language and 0% in Spark the last project is a pretty difficult let's say because it's kind of hybrid project combining two different other software it's a boot it's a root of trust software and additionally there is a functionality of being resource management software and apparently in the memory safe language we had two separate project doing exactly the same functionality so two of this project in the memory safe combined together gives more or less the same functionality in the same code size of the software written in Spark so we spent more or less the same amount of the time frame four weeks plus less than two weeks and five weeks in Spark so more or less the same time frame we found around 40 bucks in the memory and safe language and 28 bucks in Spark again big benefits and so in the recap that's a conclusion based on this average data formally verified software can be free from the memory safety problem this is star as you can see later there is still some room for abuse but in general yes it can be memory safe formally verified software has much higher quality because Spark apparently enforces a lot of attributes like secure and strict coding practice strong typing system you need to correctly internalize any data otherwise before you use it you will be like killed by the compiler you cannot use it and also what is worth to mention Spark is not a silver bullet you just see that you can apply and all of your problems disappear it's a pretty heavy software programming language so you can just sit down and write a code like in the C you write a function you write another function no you must be really sit down think about the software design it properly map any object and then when you have that then you can start starting to compile them together and write a software so you need to keep this in mind additionally Spark can prove that there is no dynamic checks cannot fail there is a something called absent of front-end errors and depends on your level of assurance you might have warranty they will never appear so this checks might not be in the binary because you don't need them anymore also it enables much more efficient security efforts because at first you will not see dummy bugs there like we sometimes see in the memory safe software and something which is not verified or unprovable is very clearly marked with the attributes so we just focus on this function what is unproved and what is unverified and focus there and there is also something called speak condition post condition ghost code I don't want to go into details on that but essentially can clearly define the state of the software in that specific point of time so you know what to expect from the software and how to behave you just know what the purpose of the specific software state machine and what also to mention is that most of the bugs which we found in Spark requires apparently very deep knowledge and understanding of the software so in the end of the day the bugs which we found are very deep type of the bugs you have architecture issues design issues and if you look from the statistical perspective when we do review the project in the memory safe language on average in four weeks we found around 40-50 bugs while in Spark we spent six weeks which is longer on average we found around 5-10 bugs which you can see there is a there is a benefits which you can see internally in our company so what is the real bugs what are the example of the bugs which are speaking about here so yeah former verified software can produce you the software which is very strong but there is always but so let's look at this but in the Spark so first problem is a problem the signature verification which we found in one of the project so there is a function who calls let's say verify public key and this verify public key has a specific checks if the software is configured to verify the signature then it verifies the signature so what is this root of trust for this function of verify signature let's take closer look and we can see that this function get authentication has apparently three states which is state authentication known authentication RSA there is also state authentication unknown but the function verify public key never takes into account this third state so is this state even possible to appear because if you have authentication RSA everything is fine authentication known we don't need to verify so it's okay what about authentication unknown and apparently the root of trust authentication unknown it's coming from the register on the hardware and register occupied three bits but three bits gives you eight states not two states so eight states apparently means that authentication unknown will be assigned to six states of this hardware not so and these states these six states are never taking into account in the verify public key because we only take into account verify known and verify RSA so what happens if you have authentication known apparently the software will treat this in the same ways authentication known so in the out of eight states only one state enforces signature verification and seven states are handled as there is no verification at all and again Prover will not be able to catch that because it's a logical error it's a logical error how it's defined by the developer so this type of bugs you can still have here and this is a problem with compiler which Alex speak more about one of the projects we reviewed had fault injection protection in scope so the code must incorporate some kind of mitigation against fault protection it's true to enable this fault mitigation here you see the assembly of the binary that we analyzed we see some memory compare function implemented in a constant way so that we this is protected constant time execution but at the same time we see a single point of weakness which is definitely a bad thing if you care about fault injections so what happened here we analyzed the source code and saw that we implemented everything correctly but for some reason compiler optimized out certain functions which weakened the protection so this was essentially a compiler problem and you only can see that in the binary so that's why you not only have to analyze your source code but the binaries yes and that's another interesting example of the issue it's not a one issue we found very small issues here and there but then we realized when we combined them together we found a very serious security issues it's a problem with the auto-utilization problem with the absent-of-random error problem with the design and performance and then in the end when we mixed them together we found something interesting so first and first Spark of course cannot prove the correctness of some metadata coming from untrusted sources like from the external media from the ROM because how it can you don't know what's there but although if you want to prove such kind of software you can provide this knowledge to the provers so the prover know what are the limits or what are the bounds check of specific untrusted data and this is what the developer did here they essentially provide some manual verification for specific contracts to help prove or prove what they want to be proved essentially so what was verified there essentially they verified the maximum size of the external media to not cross through the out-of-bunt of the memory they also verified what the local buffer is what the minimum size is there are some other checks which are boring so I didn't include there but there is also you cannot start reading from the beginning of the media but from the offset of the media so you also don't want to go out of the media size so all of that is there and in short all of this sanitization for the prover allows you to read the data between X and Y then they will pass the check and the prover will be happy then and X apparently was some kind of small number let's say 8 bytes Y always warranties that you never go outside of the media size so everything is fine it's okay so far we just have some bounce check and the prover can prove it's okay and then what we saw when we starting to execute further this function they starting to read from external media some image and this image had another header inside which had different size that the minimum size verified by the prover because the minimum size of this header was 512 bytes not 8 bytes which essentially means that some portion of the data if you read will be not really internal representation of the buffer and internal states of the buffer based on this header also won't be internalized because you just didn't read them so you cannot parse them etc etc but because before you wanted to reference any memory in Spark or if you want to use any type system in the Spark you must internalize them because otherwise you will not even compile the software so what happens I mean prover will be unhappy if you do that and then the developers force internalization so they zero this memory so it's fine yes we just zero the memory which you don't use so it's fine yes so let's go forward what we see that somewhere in the middle later on the stage execution we see the function who also tried to verify some pieces of the memory from this second image which you read and this is pretty interesting function because first thing first they internalize the entry point to be always success should be failed but they make it success so okay second thread flag they said okay if you already verified some port of the image why you want to re-verify it again so if it's already verified we have some local cache don't verify anymore performance improvements and just go to exit and return success but there is also as you can see there is ID zero this ID zero is internal representation of the state based on the header which you read in the second image and because you never fully read this image this ID was internalized by zero probably written by different team assumes that this ID in the internal memory representation is zero you means there is some performance improvements in internal state so go out and never verify anything so in the end because of this authorization the zero was there and you never verify the image and the other say verification never happened it skipped let's see another example of the bug so this one is a memory initialization code and you see that the developer for some reason decided to make a certain piece of memory readable for both super user mode and user mode so basically there is a lack of memory isolation between these two modes but problem was that spark didn't know the context of this code so it was a fine code it compiled correctly but since there was no context prover didn't catch any kind of issue with that so it's a logical error we didn't want this memory to be readable by both user and supervisor mode but since there was no good model of the hardware the prover could not find this problem but it's possible to build such knowledge via ghost code but it's very difficult to do another example of the issue is in this code that performs initialization of the tasks during task switch and you see that certain features of the cache management have been enabled to be accessible from the less privileged mode and also the cache is not invalidated on task switch so it gives less privileged mode an ability to perform side channel attacks again without a good hardware model the prover could not catch that so essentially if you write the software in Spark you also should care about the hardware model everything otherwise the prover might be blind so this knowledge is possible to be done but it's difficult so that's another problem which we found it's pretty interesting so as I mentioned we developed some specific operating system in Spark and this works on the top of the custom risk 5 microprocessor we also developed in Nvidia and this is a problem which we found during the shared memory I don't want to go to the details how this entire operating system works because we can have another talk about that but it's already public it's nothing new that we disclose here and there is a talk made by the Marko Mythic who fully goes over all of the details how this operating system works written in Spark in short just to recap this is architecture you have a hardware hardware is sliced by specific sub portion of the hardware and this sub portion of the hardware is being seen as exclusive independent hardware for each of the software partition and the Spark code is a part of the separation kernel and the separation kernel essentially enforces the limits of what the partition can have access to or not and because it's formally proofed and formally verified we have warranties that we didn't miss anything that what we divided and sliced it's exclusively only accessible for that specific software partition so we can have multiple partition that each of them have exclusive view of some specific portion of the hardware and we prove there is no way other parts of the hardware can come than that so essentially everything when you verify it looks fine and looks okay but then we realize that from the performance regions which of course make sense if you have the shared libraries used by two separate partition we do not want to lose the memory and map the same shared library twice in the different physical page yes so you just share the same page so you have a shared page between the various partition if they use exactly the same shared libraries they not only include the text section but they also can include the data section and the data section could be read and write yes so if it's read and write and depends on the shared library we might have interesting information there this interesting information might include the global state of specific shared library which could be taken into account in the logic of execution of the specific software in the partition they also might have utilization data they also might have some control flow data and save language pointers and this is pretty getting pretty interesting yes so apparently spark and the prover cannot know what you physically do with the content of this shared library inside of the partition because how so essentially this opens the room for abuse and depends of course what is in this shared memory and what is in this shared library and also what is in this shared global data so we found a few interesting bugs in our use cases and we decided to develop concept exploit against some of this shared libraries in this operating system written in spark and we wanted to show you how it works I'm not sure what will be the quality of the of the of the image here but let's try so this is apparently can I ask for a help some of the goons because when I switch they should the video mode somehow now you have ok apparently it worked so what we see here I'm not sure how much you can see here but this is software like a partition one what I was explaining before this is in the sea written partition one it's not very complicated as you can see here this is one partition main and there is also trap handler because if something screwed up we want to you know handle the exceptions and what you can see in this partition one we just first we trying to define the pointer with specific address of the memory and you can see the address of the memory is a shared buffer this is a shared buffer which is visible in the partition one and partition two and this is the address of the shared buffer a virtual address of course 18 1000 so we define the pointer here exactly to point somewhere in the middle of the shared library which is exactly in the page where this shared library is it's 1, 4, 10 essentially so it's inside of this we point somewhere inside of the shared buffer which is visible in the both partition and then inside of the shared buffer we will write some value and we write this value in the partition two there is definition where the stack page is and the stack page is mapped and the virtual address 18 5000 so we write to the shared buffer address of the stack that's all what we do in partition one which is the partition to partition two so that's what the entire software does this is the magic tool which we use internally in the NVIDIA to be able to debug or verify specific hardware specific software so we run this magic software let's say to be able to connect to the RISC-5 engine we see RISC-5 engine to be clear we check in the DMS clock you see there is nothing there it's just clear state of the RISC-5 and you can see it's clear state but it's still running it's here it's not halted we still RISC-5 is running so what we do now we try to reflash the firmware of the RISC-5 engine in the GPU to exactly have these two partition running together under separation kernel software which is from a verified and so you can see after reflashing there is some censorship which we needed to put but logic I guess it's visible you can see that it's something happened you see the core is started everything is fine and you can see the RISC-5 status is not halted after reflashing of this new firmware it's running but when you see the DMS you see the partition 2 crashed and we have stack overflow and it's formally verified software and formally verified language and you can see be able to do stack overflow that's interesting so let's check the specific page where we write so you can see when we done the software that the page of the stack page is the physical page which is only visible in the partition 2 it's not visible in the partition 1 we were managed from the partition 1 just put the pointer to the stack and overflow the stack of the memory which you don't even see after the partition switch happens so you can see it's exactly the address what we overflow so let's check again this is the address of physical page and if you reset the engine and you check again the DMS we see it's nothing there so we are not really running the firmware which we designed to run and yes and then again verify the address to be sure this is what we did so you see in the partition 1 we only write the address of the physical page where the stack will be mapped in the partition 2 which we don't see in the partition 1 and the address of the page physically matches so that's all what we did here and this exactly page is mapped as a stack so that's the proof that this is a stack page so yeah we are here first forward so just to summarize everything at first we would like to thanks NVIDIA for developing such an amazing execution environment that we can analyze we want to thanks offensive security research team we want to thanks the GPU software security team we want to thanks the product security team and ADACOR for creating such a brilliant language and everyone who was involved in this research and to summarize what we did the use of the type safety language like formal verification can minimize the attack surface not only for the memory safety issues but for other issues as well but it's not a silver bullet as you can see here there is also other issues and we need to keep this in mind also formally verified software has a much higher quality thanks to enforcement and also can prove that dynamic checks cannot fail if you have assurance of silver plus and also it enables much more efficient security efforts in short most of the bugs which we saw requires like a deep knowledge and deep understanding of the software and also hardware not only software you need to analyze entire execution environment in the details and as a result the bugs which we found it's a more architecture bugs more design issues more deeper problems essentially and again in short just to repeat again the summary of the reviews like if you lose memory safety language we internally found around 40-50 bugs in average during the review in the time frame of 4 weeks in the memory safe language we found only 510 even if you spend 50% more of the time on average but the bugs which we found is better quiet of the bugs so that's all thanks and we could take some question I think we still have 4 minutes so the question is how many bugs in Spark we found in Nvidia when we analyzed the software written in Spark so in general we haven't seen any software where we did not find the bugs that's what we can say so essentially every software which is written have some bugs we haven't seen anyone without the bugs although it's worth to mention that the software which we write usually it's a huge in scale it's complicated and we also have a custom hardware so this is very difficult to model so most of the bugs we found in this area how many of them we cannot say the numbers certainly it's significantly lower than in the memory safe language in memory safe sorry thanks


Well, hi, everybody. I'm Andrew Harrison. I'm the lead IT DevOps engineer for Omnitrax and team lead for the Agents of Change. And I'm Brian Tominson, a senior consultant in container infrastructure at Red Hat. And we're going to talk today about how Omnitrax was able to implement OpenShift to achieve a lot of the goals we've been working on for the last year. Quick history about our company, get the way back machine, go back to 1983. We created the first routing optimization system for the short haul and last mile industry. In 88, Qualcomm created a system called Omnitrax. It was the trucking, reporting, transportation reporting and compliance system that was initially the acronym. We developed on that and turned that crank for several years. Between 2006, 2012, Qualcomm and another company, RoadNet, expanded their dominance in the market. And in 2013, Omnitrax was acquired by Vista Equity, at which point in 2014, we were able to merge with RoadNet and XRS. And all of that to say, we've acquired a lot of companies over the last few years from 2014 to 2019 trying to manage that M&A multi-cloud, multi-environment space was very difficult. So in the last year, we've been working on the Omnitrax One project, the first unified platform of all of those various systems, all those various companies. And OpenShift was a major part of that. And our tight cooperation with Red Hat was a major part of that success as well. Quick piece about where we operate in most of North and South America. We have a large presence in Brazil and in Canada as well. So starting out about just a little over a year ago, what we had, what we were building on, most of it was on VMware, almost 4,000 VMs spread out across a mix of everything. We had VCF, we had Vblock, we had standard ESX hosts, some automation with V realized automation, not a lot. A lot of it was manual. We had a little bit in AWS, but everything that was there was, again, just something manual that somebody had spun up, a lot of shadow IT going on there. All of our management, all of our project management style was all waterfall, had these huge monolithic apps, isolated tower groups that didn't communicate well, didn't work well together traditionally. Had people in them that wanted to collaborate, but the mechanisms weren't there. And everything was always very driven towards a timeline rather than a goal or a project. That's where we came from. In the last year, one of the major things that we did was switch to OpenShift. We decided to containerize everything. We wanted to create a microservices platform for our company. We chose OpenShift originally, it was 3.11, that was available, what was available at the time. As soon as OpenShift 4 was in tech preview, we had it in our environment. I don't like making declarative statements. I've been told by other people inside Red Hat that we were the first to roll it into production, take that for what it's worth. We rolled it out into production very early on. We've been doing it for a long time, in terms of how long it's been in existence anyway. With OpenShift 3.11, we were able to get immediate cost reduction because we moved everything out to AWS, got rid of on-prem costs immediately. We wrote customizable playbooks to make sure that everything was infrastructure as code and that it was always adept and repeatable. We were able to provision and interact with new infrastructure that way. We reduced our environment deployment time from over a week to less than two hours. And we had a real total transformation in the IT department and especially in our organization, our team, the agents of change from the traditional waterfall style to a real agile methodology which greatly reduced all of our release times and everything else. When OpenShift 4 became available, we're currently using 4.118. We have 4.22 in sandbox cluster right now, which is kind of nice. Using the UPI installation, we reduced our deployment time from two hours to 40 minutes. We were able to manage and extend the cluster farther by built-in operators. We had a lot more cost reduction by using the CoreOS model for the master nodes so less licenses to worry about rail nodes. Direct line to architecture and design teams through Red Hat Consulting through the other members of Red Hat to work on our team. And for the maturity of that agile process that I was talking about before and making our true CI CD pipelines possible. May I hand over to Brian here for a minute to talk about how we operationalized OpenShift, utilizing operators in Ansible, Brian? Yeah, so one of the things that we ran into is in the OpenShift 3 world, you had OpenShift Ansible and sometimes that would take hours to run. There were a lot of quirks, a lot of moving parts because you had to accommodate every base use case that was out there. So with OpenShift 4, of course, you've got the IPI and the UPI installers and user-provided infrastructure and the installer-provided infrastructure. So at the time, only UPI was available for AWS. So what we ended up doing was, so what we ended up doing was we took the UPI, we wrapped it up in Ansible. And our first pass at that was successful and worked out pretty well. But then we decided we can do better. So we ended up going and taking our Ansible playbooks and setting it up to be modular and our repo and everything. We treated it just like any other software project. So our infrastructure is treated just like software. We version it, we release it, test it, everything. Operators came in really handy with that because an operator workflow is real simple. You just set up a CR and off you go. So we were able to greatly automate management of the cluster. We actually got to replace a bunch of our playbooks and then spun up a few new ones. We ended up running into a little bit of an issue and that was with getting the dev team set up and everything. There was a bit of a learning curve on OpenShift 4 for them. So in an effort to make life easier for everybody, including ourselves, we actually built an operator that they use that they can go ahead and deploy all of their pipelines. They can deploy their applications. They maintain everything as infrastructure is code. The operator reaches back into BitBucket and will look for changes and automatically reconcile. So it helps facilitate GitOps in that way. It's currently a class two operator so it can do seamless upgrades. We're working on how to get it into class three but the cool part is is because it's an Ansible operator the developers can go ahead and just fork it and make it service specific if they needed to or they can just use the generic functionality. Next slide. As far as Ansible goes, we have a very strict model on our team. Basically if it doesn't exist in Ansible, it doesn't exist. So we spent a lot of time getting the underlying OpenShift infrastructure set up and managed and beforehand, you know, and Andrew can clarify on this but they didn't really have a lot of automation around their old infrastructure. So this was kind of a new thing having everything just defined in code. We modularized the Ansible playbooks so we basically have a main, we've got config, we've got ops, we've got add-ons and things like that and these are all get sub modules under main. So any specific stuff goes into there and then we let the UPI do its thing and then our config repo runs and takes care of setting up, for example, active directory, logging, all that sort of fun stuff and then add-ons adds on a bunch of operators that we have that we like to use or to help with quality of life issues for the devs and so on. We can go from deploy.yaml in our main repo to an operationally ready cluster in 40 minutes now which is just absolutely amazing because we can tell the dev teams, hey, we're standing up a new cluster, go ahead and tag your repos now and by the time the cluster's up they're ready to rock and roll. Absolutely. Yeah and like I said, we release our infrastructure the same way that we release software.  We really stuck to an operational excellence model, we really tried to step up on that and we incorporate everything from hash core vault for security stuff and secrets management, splunk logging and all these different things so we really go through not just day two operations but day two through 30 as far as the care and feeding of a cluster. The operator model did not change the fact that we still needed Ansible to do some things, we templatized a lot of CRs so now a lot of things we wanna do, it's just one command and it makes it really easy to delegate out to developers different tasks that they wanna do. Next slide. So yeah and then so today we had that slide a few minutes ago talking about what we had, it was that spread out environment all over the place. Today we have everything in AWS, all of our infrastructure is set up there. We're using Artifactory for our images and x-ray to scan them. We've got Victrops integrated, these are all SAS solutions we've adopted and brought into the mix. We've got Victrops involved to do notification and alerting to our teams. We took the SRE model and kind of turned it on its ear a little bit. We did not want to, we're spinning up 35 new scrum teams over the next year. We're not gonna be able to find SREs to work for each of those scrum teams, it's not gonna work. So we took a different approach, we're using a virtual ops approach where we're embedding with these teams now and teaching them to be the ops part of DevOps. They are gonna be their own SREs, they're gonna be through the role of architecture owner, the role of team lead, they will have the ability and the proper permissions in OpenShift to spin up their own namespaces, start their own projects, apply the, give people grant access to them and all of that. So really allowing them the ability to carry and feed for their own areas, but at the same time giving them the ownership of it. So now when they are building their applications, they are actively thinking about the operationalization of it, that's a hard word to say, sorry. They are actively thinking about that. They, you know, and so they know that they can feed it in the logs in the Splunk and then get that information back, invict their ops as a notification if something goes wrong. That's just, it's just part of how they do their daily job now. Again, incorporating Splunk as well, we've got HashiCorp Vault as our secrets and certifications, secrets and certs management. All of that ties into OpenShift very well, that it's all very seamless. Sistig was something we adopted early on and because of being so far out in front of the edge on OpenShift, we've had a little bit of time to get those two working together, but we've had some great success with those guys and they're working very closely with us and with Red Hat to bring those, bring their service offering to us. It's been a good journey so far. We've got Jenkins inside the cluster as an OpenShift plugin, allowing the, again, the dev teams to own their pipelines. So we're not sitting back having to manage all of that. They own their own pipeline for their code, which has been a great thing. Again, taking some of that operational burden off of the central IT team and dispersing it inside their own team, developing that, getting everybody familiar with the operational part of it so that they can have that virtual ops rotation where you've got one person out of the sprint each time to handle that for them and not having to come to us every time they need something. That takes us up to, oh, I'm sorry, I'm sorry. There we go, lessons learned. One of the things we learned early adoption of OpenShift 4 was critical to our success. It depends on how important being out there on the cutting edge is to your company, though. It caused a lot of headaches early on. There were blockers because of external vendors not being caught up with the technology wave. So for us, we were very much looking forward, very much understanding that we were gonna be doing this for the next five years and didn't wanna get stuck in an older version. So we took that risk and by, that takes us to the second point, being very tightly coupled with Red Hat while we were doing this. They've been embedded with our teams for the last year. They are part of our team as far as I'm concerned right now. And that tight coupling with them has been very key to our success. It made it possible to overcome the early adoption issues very quickly. It drove innovation within our team and within Red Hat. The stuff we were working on was feeding directly back into their development to bring OpenShift to where it is today. That transformation we talked about earlier that from traditional systems administrators in an operational role to DevOps engineers, we did that in less than a gear. The guys who were on our team, myself included, not the Red Hat guys, but the Omnitrat guys. We weren't doing this a year ago. We were traditional systems administrators in our silos. We had Linux guys, we had VMware guys, we had network guys. Now we're all on a team together. We're all doing this stuff every day. It's been an amazing transformation for the technology we're working in and for our careers, it's been great. And that tight partnership facilitated that shift very easily. Having the operators available to us it allowed us to offer infrastructure as a service to the dev teams almost immediately, almost day one. Reduced the need for a very large team. We do this with four guys. Speaking of, I was the guy who didn't include the slide about my team so I apologize, I'm gonna call him out now. I wanna thank Daniel Missel, Damon Edstrom, Don Harrington, and Charles Berry, those are the Omnitrat guys. Brian Karsten-Klassohm, Vadim Zaraf, Ben Bateson, David Lewis, Christian Pulizzi, and Madhu Mari. Thank you all for those guys. I didn't put the slide up there and that's my fault, I apologize. Brian, anything else that you can talk about with Red Hat picked up during this engagement? Yeah, I mean, so we actually learned quite a bit. We learned that maybe having three masters and three workers as a starting point isn't so great. So there were some tweaks there. We learned that the team working on the machine API and everything for AWS, people are awesome because that helped out a ton. I mean, we're able to scale up now in less than five minutes really, really easily. It's automatic, the integration with AWS. And the operators on Operator Hub are just only getting better. We've got some contributions that have gone up to, for example, the AWS services operator. There's some stuff that's, you know, we're still working on like database auth method for Vault and things like that, but we're working through it really well and it's been a lot of fun. Yeah, and that touches on another thing, is not just, you know, this partnership, not just with Red Hat, but with all your vendors. You've got, if you're going to be out in front like this with the latest and greatest versions of OpenShift, you have to have good relationships with your vendors because you're going to be going to them and saying, hey, we're doing this in a completely new way and I need you to help me get it working because it's not. And they will, they'll help you. They want to keep your business. So reach out to them and have that relationship with them and it will definitely lend you your success. Any questions? We're going to save the questions. Okay, we're saving questions. Save the questions so we can get to food. All right, oh, yes, get to food. That's much more important than questions. Thank you everybody. Appreciate it, thank you very much. Thank you so much.


Moving on to entertainment news, members of the Venezuela Ceremony of Brotherhood, known as the Dancing Devils on Thursday, June 3rd, held their annual Carpus Christi celebration by calling for the end of COVID-19's pandemic in the country and the world. A member of the Dancing Devils, Henry Gonzalez, said his prayers are for an end to the pandemic. Authorities permitted the festival because the Devils wear face masks under their decorative outdoors ceremony. Venezuela's official data shows more than 238,000 cases of coronavirus and 2,689 deaths, but many health experts think the actual numbers could be much higher.


This study found that including community members in the evaluation of clinical and translational science grants did not significantly alter the quality of the reviews compared to scientific reviews alone. Additionally, it was observed that community reviews tended to focus more on the social impacts of the proposed research rather than its scientific merit. This article was authored by Jeffrey W. Treen, Margaret Schneider, Robin Elzender, and others.


Alright folks, welcome on back and not to wrap up our week here, but of course the day before Thanksgiving, great to see all of our students and members live inside the cybergroup trading room and great to have all of us back otherwise on Facebook, LinkedIn, Twitter, YouTube, X, the works on all of our social media streams and platforms here. I'll tell you what, the office lighting now actually too bright, normally I'm like on a cave here, actually a little too bright here, but nevertheless, at Cyber Trading U, be a friend, tell a friend, make sure that you're followed and subscribed all on all of our social media streams and platforms alike there. First and foremost, happy Thanksgiving, especially to all of those here in the United States and so everyone, otherwise it celebrates to you and your lovely families here and you know, it just gives you a good chance to remind yourself, you know, why we have this day to celebrate and the chance to relax and just, you know, spend time with family and, you know, just take, take your eyes away from, you know, just the, not say the negative aspects of life, but, you know, the things that kind of frustrate us, the things that are important to us outside of family, you could kind of do away with all that for one day and just be with our family and have some fun and obviously have a nice feast. So with that said, obviously things should be a little slow here today within the market. Think of it like trading right before Christmas, you know, not as many people at least around the market today, a lot more folks just already kind of getting the cooking early, getting the preparation done in advance. So with that said, hey, this shot trade has made a nice pop back up. I said right before this meeting started at least, I was like, you know, I think this thing's going to drop off pretty soon, sooner than later, much like it did yesterday. So let's actually go to this trade from yesterday. I was wrong with that drop, at least so far, you know, sooner rather than later, I'm sure. But nevertheless, it did just break higher there.  But basically yesterday, stock went from four to eight doubled up in price, essentially, then made the Christmas tree pattern. Christmas came early here, right? Made the Christmas tree, what goes up comes right back down, basically at the same pace, if not faster. And, you know, history often repeats itself, right? So to see this make another run back up this morning after 8am in pre-market, after 8am, I emphasized because at 7.30, 7.45, this wasn't looking good at all. It wasn't going anywhere. So that's where we didn't put this on our watch list, but, hey, ended up popping a little bit at the eight o'clock move, more so it broke higher prior to 8.30, and that's what led to the, you know, at least the next squeeze up here. Let me take a look. I don't even know if I have this on my book map just yet. I was helping out one of our trial members here, just joining us on a stock, but I'm not going to look at that one as much, this shot trade. I'm going to just see what level four looks like. It takes a few seconds for it to load up. You got a big sell order out there. It looks like at least out there at 7.50 for about 126,000. We'll see how long that order has been out there for. It's going to finish loading up here in just a moment. I'm sure there we go. So it's been out there since 7am. Now that was essentially, essentially the high that we had from yesterday, right? Basically, 7.50. So no guarantee it's going to move exactly right up there, but certainly a nice run up thus far. And I would look for your next resistance not to be at 7.50, but to be like if anything around 6 whole number level. And then on top of that, you have 1617K on the order book on the heat map here at 6.50 as well. So essentially you are kind of looking at every 50 cents now at this stage, because you're more focused on whole numbers like 6 and 7.  Then you got the big kahuna here at 7.50. So it's essentially every 50 cents for the stock. Now what's interesting on this, this is the weird part, the interesting, the weird part here. So it looks like there was some news out on this stock from like late October, like October 30th. I'm just reading this out to you right now. Safe Shot shares trading higher after the company announced direct to consumer launch of safety shot in the first week of December 2023. All right. That led to a little pop at the end of October. Basically here this candle, not really a big move. But that's really the only good news that I've seen on this stock since, for example, November 15, just last week, exactly one week ago. Safe Shot Inc says due to a spin off of SRM Entertainment, limited company, or due to a spin off of SRM Entertainment, this company expects that revenues will decrease from basically a million dollars to $800,000 20% drop off. And they expect that there will be a significant increase in the net loss of the company from 6.7 million to 9.4 million. You tell me how that makes sense. So that's the only good that's the only news I've seen on this trade really since this is just basically some sort of short squeeze where, you know, I guess maybe a larger group of day traders attack the offer, the shorts had to cover on top of that, at least as many as we're able to, I'm sure a bunch got blown apart on this trade. And, you know, it actually moved up towards all time highs yesterday, right? Setback from February of 21, 752. Yeah, it got real close there yesterday, right? Just like a penny away, a penny or two away.  So that's what I was saying, few folks to be careful on this stock just because VSME, I brought this up yesterday as well. This stock was a new IPO as well and broke out over resistance and then pulled back the same day. Look where it's at now. So you don't want to get stuck on a trade like shot. You know what, I guess I kind of am forcing my hand here to add this to our watch list. I've probably put it towards the middle or towards the bottom here by the end of it all. Hopefully there's just stocks that aren't as exhausted yet or haven't made a big move up and down already have some potential there. Yehuda says they're launching a product on the West Coast. Okay, let me take a look at this here really quick because I didn't know if there was any additional news that were sent out there. I'll take a look at that if anything after the meeting there. You know, our whole focus at Cybertrading University is to follow the big money. So that includes icebergs that includes that obviously being level three, level four time and sales included. So we'll take a quick look at least just after the meeting finishes up. Now that said the shots on our list not probably probably won't be near the top of our watch list for right now but I'll tell you what the market was pushing up a little bit here. We were moving up pretty nicely early in pre market this morning. You know getting closer towards that 455 and actually laying above it as of now. I think that we have stronger resistance ahead. I said this earlier in the week around 457 and change a little over 457 maybe even close to 58. If I'm not mistaken, let me double check my lines here. They're up on this one. Yep. 457 79 plotted these levels going into this given week. So you know, I did say 455 could be could be a potential level but you know, honestly, I do think that we can push up a little bit more and test that 57 change. But what we'll do is go from top to bottom. Now folks really just rip it from the gainers and losers list here. See if there's anything looking good. I mean the SPRC was looking really nice at first in pre market but then fell off and then fell flat. There is some news out on this company I think just with a launch that they're doing in Israel or they're doing a deal with a vehicle importer company based in Israel. Alright, so nice, I guess collaboration partnership. Perhaps that brings big business to this company and led to a nice pop at first. You know, it's still up a lot. I hope the order book fills in a lot more once the market does open. That would make this a lot more trade. But yeah, I'll add this here to our list as well as PRC. Now, here's the thing. Follow me ready. This right here is like the percent gain column like how much a stock is up percentage wise. It might be tiny font. So if you can't read it, my apologies. Your top percent gainers up 24%. What does that tell you? What does that tell you right there?  SGD this had popped pretty nicely earlier this week from last week to but similar deal with shot. You know, that's a pop and drop stock and unless it's directly making a strong run up like the shot trade is right now, I wouldn't be as inclined to give it another go. Man, we're already basically 5% here folks at this point. I filtered out my volume criteria here as well. So there's no like light volume stuff. At least all of these are trading over 100k. Had a couple callouts in the chat just mentions like AI was you know up this morning and PLTR is up this morning and my Mara was up a little bit all with the market mind right. I would say PLTR I could you know put on our main list just because it's not really expensive. It's extremely liquid meaning it's gonna have as good of a spread as you see here. If not better like more filled in order book by the time the market opens up. So not only that we're also very familiar with this trade. So that's where I'll kind of give this a small exception. I'll put this on our main list right now. If you do well on AI day to day then you know who you are. If you do well on Mara day to day you know who you are. I could say that on a litany of different trades. So this is where I'd say start and stick with what I'm putting on this watch list but hey if you'd rather follow the market in general and if you're expecting a pop up like I am then perhaps you could be inclined to follow a stock from your side list. Let me ask really quick I I know who's saying yes to this because I seem in the chat board who here follows Tesla who here trades Tesla here perhaps on a day to day basis week to week basis you know who you are and it's not going to be everyone inside our live trading room but it's going to be a few of us it can be a couple of us right Gary Jeff Chuck I'm sure John's in there somewhere. So hey if none of these stocks none of the three I'm going to put on the watch list really fancy you and if there is a stock that's moving at least in pre-market Tesla perhaps or an AMD obviously oh actually I put this on the pre-market list I just kind of reminded myself in the back of the head. So one last one we are going to add to our list here this year and obviously with NVIDIA earnings you know SOXL is a semiconductor ETF it's a chip ETF so we always follow this but actually I just thought of this right now before we finished up. So obviously NVIDIA posted earnings at a double beat and AMD at a double beat like a week or two ago as well so it leads you to say like all right well if the market's pushed this should definitely make a nice new run up after hours were crazy yesterday with the pop then drop then pop back up again so you know if it's too volatile for you I understand but SOXL definitely I'll put spotlight on and hey again if you trade NVIDIA if you trade AMD and obviously like I said like a Tesla on top you know perhaps that could be more up your alley today on a day like today. Yeah there we go John from Kathleen GDC pop yeah it's up 17 percent and definitely a timely call out from Kathy or one of our very good traders inside our room actually so with that you know what I am going to put this on our list popping right now for us direction up and with that hopefully the order book fills in more once the market does open here so hey if it pulls right back down and then we'll scrap it but not bad it's very good to call out timely from Kathleen and yeah absolutely we'll put this on our list for now. All right so folks let me know if there's anything else up down left right more than five percent that you'd want me to look at there just like GDC just like GDC let's take a look here just on the volume scan I have there's that GDC there we go looks like we would have caught that there Kathleen a step ahead not really much else though otherwise so that's fine that's fine folks we got a great list though at least pre Thanksgiving especially with like honestly I was wondering I was like why isn't a video doing earnings two days before Thanksgiving like it's the weirdest thing ever right like I'd rather it honestly just be the week before where we had the CPR report we had all bunch of different stuff happening more earnings to be announced from last week but you know what it actually gives you a little volatility a tiny little sliver of volatility for this morning so perhaps we could see at least a movement up within the market and stocks like PLTR obviously the video and the ETF SOXL and a couple more look to move with it but hey best of luck trading here going to the market open folks happy Thanksgiving again to anyone obviously that celebrates all around the world of course to all of us here within the United States to you and your lovely families and hey we look forward to seeing you back at least on Friday remember Friday we have a half day within the market if you're not going to be here no sweat enjoy the long weekend then obviously but we will be here as normal right inside the live trading room early at 7 30 Eastern again if you're interested in joining our live trading room just for all of us on social first and foremost follow us at cyber trading you be a friend tell a friend look to subscribe and follow us first on social media at cyber trading you will be back at 2 30 this afternoon at least but otherwise if you're interested in joining us inside our live trading room see our students like Kathleen Abdul Ravina Margaret Leda etc and all of them otherwise just scan that QR code on the top left of your stream with your phone get you access to all of our students and traders there alright folks but again best of luck trading going into this morning I'll be back on for all of us there at least inside the cyber group room just about 15 minutes take care