https://github.com/PLSysSec/FaCT

Skip to content Toggle navigation
 
Sign up

  * Product
      +  
        Actions
        Automate any workflow
      +  
        Packages
        Host and manage packages
      +  
        Security
        Find and fix vulnerabilities
      +  
        Codespaces
        Instant dev environments
      +  
        Copilot
        Write better code with AI
      +  
        Code review
        Manage code changes
      +  
        Issues
        Plan and track work
      +  
        Discussions
        Collaborate outside of code
      + Explore
      + All features
      + Documentation
      + GitHub Skills
      + Blog
  * Solutions
      + By Plan
      + Enterprise
      + Teams
      + Compare all
      + By Solution
      + CI/CD & Automation
      + DevOps
      + DevSecOps
      + Case Studies
      + Customer Stories
      + Resources
  * Open Source
      +  
        GitHub Sponsors
        Fund open source developers
      +  
        The ReadME Project
        GitHub community articles
      + Repositories
      + Topics
      + Trending
      + Collections
  * Pricing

[                    ] 

  *  
    #
    In this repository All GitHub |
    Jump to |

  * No suggested jump to results

  *  
    #
    In this repository All GitHub |
    Jump to |
  *  
    #
    In this organization All GitHub |
    Jump to |
  *  
    #
    In this repository All GitHub |
    Jump to |

Sign in
Sign up
{{ message }}
PLSysSec / FaCT Public

  * Notifications
  * Fork 12
  * Star 139

Flexible and Constant Time Programming Language

License

BSD-3-Clause license
139 stars 12 forks
Star
Notifications

  * Code
  * Issues 1
  * Pull requests 0
  * Actions
  * Projects 0
  * Wiki
  * Security
  * Insights

More

  * Code
  * Issues
  * Pull requests
  * Actions
  * Projects
  * Wiki
  * Security
  * Insights

PLSysSec/FaCT

This commit does not belong to any branch on this repository, and may
belong to a fork outside of the repository.
master
Switch branches/tags
[                    ]
Branches Tags
Could not load branches
Nothing to show
{{ refName }} default View all branches
Could not load tags
Nothing to show
{{ refName }} default
View all tags

Name already in use

A tag already exists with the provided branch name. Many Git commands
accept both tag and branch names, so creating this branch may cause
unexpected behavior. Are you sure you want to create this branch?
Cancel Create
13 branches 0 tags
Code

  *  
    Clone
    HTTPS GitHub CLI
    [https://github.com/P]

    Use Git or checkout with SVN using the web URL.

    [gh repo clone PLSysS]

    Work fast with our official CLI. Learn more.

  * Open with GitHub Desktop
  * Download ZIP

Launching GitHub Desktop

If nothing happens, download GitHub Desktop and try again.

Launching GitHub Desktop

If nothing happens, download GitHub Desktop and try again.

Launching Xcode

If nothing happens, download Xcode and try again.

Launching Visual Studio Code

Your codespace will open once ready.

There was a problem preparing your codespace, please try again.

Latest commit

@scauligi
scauligi Merge pull request #65 from vbgl/compat-with-core-0.12
...
b3daa03 Feb 18, 2022
Merge pull request #65 from vbgl/compat-with-core-0.12

Ensure compatibility with core >= 0.12

b3daa03

Git stats

  * 1,085 commits

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
Unity @ 994779f
 
 
docker
 
 
example
 
 
src
 
 
test
 
 
.gitattributes
 
 
.gitignore
 
 
.gitmodules
 
 
.merlin
 
 
FaCT_extended.pdf
 
 
LICENSE
 
 
Makefile
 
 
README.md
 
 
_oasis
 
 
_tags
 
 
guidelines.md
 
 
myocamlbuild.ml
 
 
ocamlswitch.txt
 
 
View code
[                    ]
FaCT Useful links: Building Virtual machine image Using Docker
Setting up the build environment Using a local environment 1. Install
System Dependencies 2. Install OCaml + packages 3. Configure Paths
Compiling FaCT Usage Basic Usage Link to a C library Debugging
Acknowledgements

README.md

 FaCT

This is the compiler for the Flexible and Constant Time cryptographic
programming language. FaCT is a domain-specific language that aids
you in writing constant-time code for cryptographic routines that
need to be free from timing side channels.

 Useful links:

  * Our paper
  * Online demo using Compiler Explorer (source forked from
    mattgodbolt/compiler-explorer)
  * FaCT case studies / evaluation
  * Haskell embedding
  * Python embedding
  * Vim syntax files

 Building

To build the compiler, you can either build from source or download a
pre-built release. We recommend building from source if possible.

 Virtual machine image

You can download a VM image pre-configured for building the FaCT
compiler and case studies. The file fact.ova should have a SHA256 sum
of 089398c85c5074d911c2f2b67ca22df453235e8733f1eb283c71717cf70f714c.

 Using Docker

If you have docker installed, you can load our docker image with the
build environment already installed:

cd docker/
./run.sh

Once inside the docker shell, run the following to finish setting up
the environment:

cd FaCT/
eval $(opam config env)

 Setting up the build environment

FaCT is developed using OCaml 4.06.0 and LLVM 6.0.

 Using a local environment

Building FaCT has been tested on Ubuntu 16.04, 18.04, and macOS.

 1. Install System Dependencies

Ubuntu (16.04 & 18.04)

sudo apt install llvm-6.0 clang-6.0 cmake libgmp-dev m4 pkg-config

macOS

These instructions require Homebrew

brew install cmake gmp m4 pkg-config
brew install llvm@6 --with-toolchain

Note: This does not put the proper version of clang on your PATH. You
will need to run:

export PATH="$(brew --prefix llvm@6)/bin:$PATH"

 2. Install OCaml + packages

We recommend installing the opam package manager to manage OCaml and
package dependencies:

sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

Then, install OCaml and the libraries:

opam init
eval $(opam config env)
opam switch create 4.06.0
eval $(opam config env)
opam switch import ocamlswitch.txt

Finally, make sure the Z3 lib is available to the OCaml compiler:

export LD_LIBRARY_PATH="$HOME/.opam/4.06.0/lib/z3:$LD_LIBRARY_PATH"

 3. Configure Paths

The FaCT compiler depends on the LLVM 6.0 toolchain at runtime, and
expects binaries with -6.0 suffixes. Ensure that clang-6.0 is in your
PATH:

clang-6.0 --version

 Compiling FaCT

You can now build the compiler:

oasis setup
make

This will produce the factc executable.

 Usage

 Basic Usage

Run ./factc <source files> to compile a FaCT program.

 Link to a C library

FaCT is designed to be called from C code. Compiling FaCT source
files will output an object file, which can then be linked to a C
file. As an example:

cd example/
../factc -generate-header example.fact
clang-6.0 -c main.c
clang-6.0 -o final main.o example.o

You can then run the executable:

./final

 Debugging

Many debugging options and intermediate data structures are
available. Run ./factc -help for all options.

 Acknowledgements

We thank the anonymous PLDI and PLDI AEC reviewers for their
suggestions and insightful comments.

About

Flexible and Constant Time Programming Language

Resources

Readme

License

BSD-3-Clause license

Stars

139 stars

Watchers

15 watching

Forks

12 forks

Releases

No releases published

Packages 0

No packages published

Contributors 11

  * @scauligi
  * @soelgary
  * @bjohannesmeyer
  * @YunluHuang
  * @amirian28
  * @deian
  * @vbgl
  * @djrenren
  * @kwantam
  * @alex-chew
  * @ntauth

Languages

  * OCaml 80.3%
  * C 15.5%
  * Standard ML 1.3%
  * Shell 1.2%
  * Other 1.7%

Footer

 (c) 2022 GitHub, Inc.

Footer navigation

  * Terms
  * Privacy
  * Security
  * Status
  * Docs
  * Contact GitHub
  * Pricing
  * API
  * Training
  * Blog
  * About

You can't perform that action at this time.
You signed in with another tab or window. Reload to refresh your
session. You signed out in another tab or window. Reload to refresh
your session.