Currently AWS uses a SMT solver to decide on public/non-public policies https://aws.amazon.com/blogs/security/protect-sensitive-data-in-the-cloud-with-automated-reasoning-zelkova/

Learn about SMT solvers & see how feasible using a smt solver is for supporting the more minimal policy set in ceph object storage RGW

Looking for hackers with the skills:

c++ s3 smt z3

This project is part of:

Hack Week 19

Activity

  • almost 5 years ago: abhishekl added keyword "z3" to this project.
  • almost 5 years ago: abhishekl added keyword "smt" to this project.
  • almost 5 years ago: abhishekl added keyword "c++" to this project.
  • almost 5 years ago: abhishekl added keyword "s3" to this project.
  • almost 5 years ago: abhishekl started this project.
  • almost 5 years ago: abhishekl originated this project.

  • Comments

    Be the first to comment!

    Similar Projects

    Port some classic game to Linux by MDoucha

    Let's pick some old classic game, reverse engineer the data formats and game rules and write an open source engine for it from scratch. Some games from 1990s are simple enough that we could have a playable prototype by the end of the week.

    Write which games you'd like to hack on in the comments. Don't forget to check e.g. on Open Source Game Clones, Github and SourceForge whether the game is ported already.

    Hack Week 24 - Master of Orion II: Battle at Antares & Chaos Overlords

    Work on Master of Orion II continues but we can hack more than one game. Chaos Overlords is a dystopian, lighthearted, cyberpunk turn-based strategy game originally released in 1996 for Windows 95 and Mac OS. The player takes on the role of a Chaos Overlord, attempting to control a city. Gameplay involves hiring mercenary gangs and deploying them on an 8-by-8 grid of city sectors to generate income, occupy sectors and take over the city.

    How to ~~install & play~~ observe the decompilation progress:

    • Clone the Git repository
    • A playable reimplementation does not exist yet, but when it does, it will be linked in the repository mentioned above.

    Further work needed:

    • Analyze the remaining unknown data structures, most of which are related to the AI.
    • Decompile the AI completely. The strong AI is part of the appeal of the game. It cannot be left out.
    • Reimplement the game.

    Hack Week 20, 21, 22 & 23 - Master of Orion II: Battle at Antares

    Master of Orion II is one of the greatest turn-based 4X games of the 1990s. Explore the galaxy, colonize planets, research new technologies, fight space monsters and alien empires and in the end, become the ruler of the galaxy one way or another.

    How to install & play:

    • Clone the Git repository
    • Run ./bootstrap; ./configure; make && make install
    • Copy all *.LBX files from the original Master of Orion II to the installation data directory (/usr/local/share/openorion2 by default)
    • Run openorion2

    Further work needed:

    • Analyze the rest of the original savegame format and a few remaining data files.
    • Implement most of the game. The open source engine currently supports only loading saved games from the original version and viewing the galaxy map, fleet management and list of known planets.

    Hack Week 19 - Signus: The Artifact Wars

    Signus is a Czech turn-based strategy game similar to Panzer General or Battle Isle series. Originally published in 1998 and open-sourced by the original developers in 2003.

    How to install & play:

    • Clone the Git repository
    • Run ./bootstrap; ./configure; make && make install in both signus and signus-data directories.
    • Run signus

    Further work needed:

    • Create openSUSE package
    • Implement full support for original game data (the open source version uses slightly different data file contents but original game data can be converted using a script).


    New KDE Plasma notification app/applet by apappas

    Description

    My memory is terrible so I depend a lot on notifications to carry me through the workday. As a plasma user I am ok with the current applet, but I don't love it. It is too small for the centrality it has in my day. Also I dislike how you can not go back to notifications you have dismissed

    Goals

    Develop a plasma app that * must gather notifications without disrupting the existing notification app * must offer the ablity to refer to dismissed/archived/seen notification up to some defined point in the past * must allow deletion of notifications


    YQPkg - Bringing the Single Package Selection Back to Life by shundhammer

    tl;dr

    Rip out the high-level YQPackageSelector widget from YaST and make it a standalone Qt program without any YaST dependencies.

    The Past and the Present

    We used to have and still have a powerful software selection with the YaST sw_single module (and the YaST patterns counterpart): You can select software down to the package level, you can easily select one of many available package versions, you can select entire patterns - or just view them and pick individual packages from patterns.

    You can search packages based on name, description, "requires" or "provides" level, and many more things.

    The Future

    YaST is on its way out, to be replaced by the new Agama installer and Cockpit for system administration. Those tools can do many things, but fine-grained package selection is not among them. And there are also no other Open Source tools available for that purpose that even come close to the YaST package selection.

    Many aspects of YaST have become obsolete over the years; many subsystems now come with a good default configuration, or they can configure themselves automatically. Just think about sound or X11 configuration; when did you last need to touch them?

    For others, the desktops bring their own tools (e.g. printers), or there are FOSS configuration tools (NetworkManager, BlueMan). Most YaST modules are no longer needed, and for many others there is a replacement in tools like Cockpit.

    But no longer having a powerful fine-grained package selection like in YaST sw_single will hurt. Big time. At least until there is an adequate replacement, many users will want to keep it.

    The Idea

    YaST sw_single always revolved around a powerful high-level widget on the abstract UI level. Libyui has low-level widgets like YPushButton, YCheckBox, YInputField, more advanced ones like YTable, YTree; and some few very high-level ones like YPackageSelector and YPatternSelector that do the whole package selection thing alone, working just on the libzypp level and changing the status of packages or patterns there.

    For the YaST Qt UI, the YQPackageSelector / YQPatternSelector widgets work purely on the Qt and libzypp level; no other YaST infrastructure involved, in particular no Ruby (or formerly YCP) interpreter, no libyui-level widgets, no bindings between Qt / C++ and Ruby / YaST-core, nothing. So it's not too hard to rip all that part out of YaST and create a standalone program from it.

    For the NCurses UI, the NCPackageSelector / NCPatternSelector create a lot of libyui widgets (inheriting YWidget / NCWidget) and use a lot of libyui calls to glue them together; and all that of course still needs a lot of YaST / libyui / libyui-ncurses infrastructure. So NCurses is out of scope here.

    Preparatory Work: Initializing the Package Subsystem

    To see if this is feasible at all, the existing UI examples needed some fixing to check what is needed on that level. That was the make-or-break decision: Would it be realistically possible to set the needed environment in libzypp up (without being stranded in the middle of that task alone at the end of the hack week)?

    Yes, it is: That part is already working:

    https://github.com/yast/yast-ycp-ui-bindings/pull/71

    Go there for a screenshot

    That's already halfway there.

    The complete Ruby code of this example is here. The real thing will be pure C++ without any YaST dependencies.

    The Plan

    • DONE: Clone libyui where libyui (high-level), libyui-qt, libyui-qt-pkg live


    RISC-V emulator in GLSL capable of running Linux by favogt

    Description

    There are already numerous ways to run Linux and some programs through emulation in a web browser (e.g. x86 and riscv64 on https://bellard.org/jslinux/), but none use WebGL/WebGPU to run the emulation on the GPU.

    I already made a PoC of an AArch64 (64-bit Arm) emulator in OpenCL which is unfortunately hindered by a multitude of OpenCL compiler bugs on all platforms (Intel with beignet or the new compute runtime and AMD with Mesa Clover and rusticl). With more widespread and thus less broken GLSL vs. OpenCL and the less complex implementation requirements for RV32 (especially 32bit integers instead of 64bit), that should not be a major problem anymore.

    Goals

    Write an RISC-V system emulator in GLSL that is capable of booting Linux and run some userspace programs interactively. Ideally it is small enough to work on online test platforms like Shaderoo with a custom texture that contains bootstrap code, kernel and initrd.

    Minimum:

    riscv32 without FPU (RV32 IMA) and MMU (µClinux), running Linux in M-mode and userspace in U-mode.

    Stretch goals:

    FPU support, S-Mode support with MMU, SMP. Custom web frontend with more possibilities for I/O (disk image, network?).

    Resources

    RISC-V ISA Specifications
    Shaderoo
    OpenGL 4.5 Quick Reference Card