Ectopass for Visual Studio Code

The Ectopass extension allows you to analyze a single C file with Ectopass and check for micro-architectural security vulnerabilities.

Given an empty workspace, launch the Ectopass: Demo command to spawn an example of a C and TOML configuration files to start with for the analysis.

Details

The command currently only support "NonInterference" as security condition to check for vulnerabilities. It checks for two things:

• if there are universal gadgets that execute in speculation (such as the one in the original Spectre example)
• if there are values marked are secrets that are leaking

To mark values (global variables or parameters) as secret or untrusted, see the security_tags section of the config.toml file.

Good to know

• The code is compiled with -Og. You might need to use temporary variables to make sure some parts are not optimized away.
• It is executed on an x86 based machine running Ubuntu.
• You will get an error pop-up with the compiler error message if your code does not compile.
• Toggle the bottom panel and go to "PROBLEMS" to have an overview of all vulnerabilities in your C file.
• The Ectopass: Demo command is only available on VS Code for the web and does not work natively.
• The Ectopass: Visualize results in ectopass-results command is only available on native VS Code and is made to visualize results of large projects. Contact us for more information.

References

@misc{mosier2021relationalmodelsmicroarchitecturesformal,
      title={Relational Models of Microarchitectures for Formal Security Analyses}, 
      author={Nicholas Mosier and Hanna Lachnitt and Hamed Nemati and Caroline Trippel},
      year={2021},
      eprint={2112.10511},
      archivePrefix={arXiv},
      primaryClass={cs.CR},
      url={https://arxiv.org/abs/2112.10511}, 
}