Ectopass for Visual Studio Code

The Ectopass extension allows you to analyze a single C file with Ectopass and check for Spectre vulnerabilities.

Given an empty workspace, launch the Ectopass for non-interference and cache side-channels command to spawn an example of a C and JSON configuration files to start with for the analysis.

Details

The command will use "non-interference" as security conditions 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, the security-tags.json file is used. { "depth": 1 } means that it is the value pointed which is the secret but not the address.

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.
• You will get an error pop-up with the compiler error message if your code does not compile.
• The extension uses a backend hosted on a free tier from Render. That means that the first execution of the command could take up to one minute to execute.

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}, 
}