SKnife

SKnife is a declarative prototype to partition multi-component applications employing information-flow security methodologies in order to exploit the Separation Kernel (SK) technology. SKnife first check the application is partitionable, i.e. do not leak data to untrusted hardware components, then finds the minimal eligible partitioning, the partitioning with the fewer number of SK domain that avoids data leak. To support the developers of non-partitionable applications, SKnife-Recommend allows finding labelling suggestions to relax the information-flow constraints in order to allow the partitioning.