Regarding no DIP generation on gate-level netlist

[rafidmuttaki]

Hi, I am working on some locked gate-level netlist to evaluate the performance against the RANE attack. I am having 2 issues with different designs. 1) the DIP is not generated for small key sizes for a long runtime (~ 1 day). 2) Same DIPs are generated in multiple iterations and no convergence occurs.

[shervinrs]

Can you share the input files here? Did you sort clk/input/output ports in the correct order?

[rafidmuttaki]

files.zip Hi,

I have attached the oracle and obfuscated netlist here. It is the case where same DIP is generated again and again without converging for several hours. I believe I have maintained the right formatting for the ports.

[shervinrs]

I see that the internal gates are instantiated using named port mapping (.A, .B, .Y) with generic gate names (nand): nand r1_U1534 ( .A(r1_n1427), .B(r1_n1428), .Y(r1_n1425) );

Can you change your benchmarks to either: 1- Use gates from your predefined library: Define module my_nand(...) in nand.v and use my_nand in aes module.

2- Instantiate gates like this (without port labels and also assigning output as the first port): nand r1_U1534 ( out, in1, in2 );

Because without one of these changes I'm not sure if Symbiyosys understands your original .v files correctly. I tried to change port names to some random name and it did not complain!

[rafidmuttaki]

Hello, Attached is the modified files you mentioned in your reply. I have also added the cell libraries and the main.py file. It still does not run at my side. Can you please check? Thanks. files_mod2.zip

[shervinrs]

This one seems to be working correctly. There are two DIPs in the first five cycles:

[16:48:37.0585 verilog2circuit WARNING] circuit: aes_128_v5, inputs: 257, outputs: 128, keyinputs: 0 [16:48:37.0598 verilog2circuit WARNING] circuit: aes_128_v5_obf, inputs: 257, outputs: 128, keyinputs: 5 [16:48:37.0598 perform WARNING] initial values for boundary=20, step=5 [16:48:37.0598 perform WARNING] timeout=7200s [16:49:05.0046 dis_gen INFO] dip: ["256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"] [16:49:05.0046 dis_gen WARNING] iteration: 1, dip seq length: 4 [16:49:05.0046 dis_gen INFO] keys: ["5'b00000", "5'b01100"] [16:50:06.0354 dis_gen INFO] dip: ["256'b0000000010110100011111011111111100100000001011001000000000100000000000000000010000100000001000001110010001001001101010110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "256'b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"] [16:50:06.0354 dis_gen WARNING] iteration: 2, dip seq length: 5 [16:50:06.0354 dis_gen INFO] keys: ["5'b10100", "5'b11100"] [14:29:17.0613 dis_gen WARNING] two different agreeing keys could not be found for the current set of assumptions, checking uc [16:52:50.0493 check_uc WARNING] uc passed! [16:54:10.0596 find_keys INFO] assigned keys: ["5'b11111", "5'b11111"] [16:54:10.0596 perform WARNING] key: 5'b11111 [16:54:10.0598 execution_time WARNING] total time: 333.04s

There was a bug with UC check in the code that is now corrected. Please update your clone. You can copy all lib files into a folder and set its path in external_lib_path in main_formal.py.

[rafidmuttaki]

Hello, thank you for the reply. I have one question regarding this. Did you use the Jaspergold solver or the yosis for this result? When running the Jaspergold, it was showing an error regarding the sequence of the bus in the main.sv file (0:max). Although I had declared them correctly in the verilog design. I will run again with your updated files with the two solvers and let you know. Thanks.

[shervinrs]

I used yosis (symbiyosys). Unfortunately, I don't have access to JasperGold right now to check it. If you can post terminal output and the corresponding temp folder in the lockbox folder, I can take a look at it.

[rafidmuttaki]

Hello, The issue still persists in my end. When I used the "nand, and, or" this cell names with (.A(), .B()) configurations, I was getting the same DIPs. But now, when I used the actual cell names from the library and the same gate level netlist I sent you, I see no iterations at all for several minutes. The logfile shows the attached screenshot.

I have added the tool configuration I am running also. Please let me know if I am doing something wrong here. Thanks. RANE.zip

[shervinrs]

Please apply modification in this link to speedup Symbiyosys: https://github.com/gate-lab/RANE/wiki/Formal-Tool-Interface#optimizations-for-symbiyosys Without these changes, Symbiyosys will take a long time to generate VCD files which are unnecessary for the attack.

[rafidmuttaki]

Hello, I have made the changes in the mentioned link. However, I could not execute:

cd symbi_attack
sudo make install

as it says .sh command not found So, I normally did the sudo make install in the same directory. Finally, I ran the RANE attack and found the following message. It shows the first iteration but then terminates. The screenshot is added with this message.

[shervinrs]

Can you upload the logfile from the lockbox folder?

[rafidmuttaki]

Hi,

I have added the logfile here. logfile.txt

[shervinrs]

That is weird. Can you test another circuit? Maybe Symbiyosys source code also changed and that modification is not correct anymore. Can you check if the replaced Python code is exactly the same with the one from the wiki page?

[rafidmuttaki]

Hi, yes. When I was editing the python code, I found that the link solution saying ".format...." part is not available in the github and in my local version. Never the less, I added that portion in my python source code. So, it was not a complete match. Can you please share your local python file so that I can compare?

[shervinrs]

Ok, I checked the current Symbiyosys code in here. They changed it. You need to remove --dump-vcd {trace_prefix}.vcd part only.

[rafidmuttaki]

Hi, I am getting the same logfile error that I shared before.

[shervinrs]

Did you make install it again?

[rafidmuttaki]

Hi, yes.

But the same error is occuring.

[shervinrs]

I tried the new Symbiyosys version with the mentioned changes and it works on my side. Can you change your engine from yices to one of the boolector/z3/mathsat/cvc4 and see if that helps? You need to install that engine from here first.

Edit: actually you can just put engine = "" so it uses the default smtbmc engine without installing anything.

[rafidmuttaki]

Hello, I have tried z3, no engine (""), and boolector as the engine. But still no solution. z3: no engine option (""): boolector: for boolector there was no DIP to be found in 2-hour runtime.

[shervinrs]

Engines shouldn't fail after removing VCD generation. That is unrelated to the engine job. Can you test with the original Symbiyosys code that was working for the first two iteration before? Also, make sure that your system are not memory restricted. Check system monitor during a run and make sure that memory usage does not hit %100. Because that could also kill the engine.

[rafidmuttaki]

Hello, Are you suggesting the initial configuration with only vcd part removed in the symbiyosis python file?

[shervinrs]

Even before that, with VCD generation to see if it can find two DIPs without error.

[rafidmuttaki]

Hi, As mentioned earlier, with the default setup, the terminal does not show any DIP and logfile says the vcd file is being written. This is the logfile after almost 8 hours of runtime. The terminal:

[rafidmuttaki]

Hi, I have run two versions of the code with default configuration. 1. with cell name (INVX1 (.A(), .Y())),

2. without cell name (not ( (), () ))

3. For case 1, no DIP is generated for more than 8 hours. The logfile: logfile_cell_name.txt

For case 2, same DIPs are generated. The logfile: logfile_direct_logic.txt

Terminal:

The netlist for case 1 is the same sent to you. Netlists for case 2: netlist.zip

[shervinrs]

The first one with disabled VCD is the preferred method. For the second one you need to make sure that port orders are correct for combinational gates. That means, output wire should be set as the first argument and then input wires after that: not (out, in) nand(out, in1, in2, ...) Also, for dff you need to check the dff module.

[rafidmuttaki]

Hi, I have run the 2 mentioned forms of the aes design without any error, finally. The change I made was only the vcd part removed from symbiyosys. I am running another design and facing a different problem: The logfile does not say much: logfile.txt

[shervinrs]

Please share the input files. Also, please create a new issue since this is a new problem.

[rafidmuttaki]

library.zip netlist.zip Hello, The netlist and used library are attached.

[shervinrs]

On my system it runs like this:

[19:11:12.0150 verilog2circuit WARNING] circuit: sha1_core_5, inputs: 516, outputs: 169, keyinputs: 0 [19:11:12.0153 verilog2circuit WARNING] circuit: sha1_core_5_obf, inputs: 516, outputs: 169, keyinputs: 5 [19:11:12.0153 perform WARNING] initial values for boundary=20, step=5 [19:11:12.0153 perform WARNING] timeout=7200s [19:11:17.0725 dis_gen INFO] dip: ["515'b01000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "515'b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"] [19:11:17.0725 dis_gen WARNING] iteration: 1, dip seq length: 2 [19:11:17.0725 dis_gen INFO] keys: ["5'b00000", "5'b00001"] [19:11:34.0304 dis_gen INFO] dip: ["515'b01100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "515'b00100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "515'b00100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", "515'b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"] [19:11:34.0304 dis_gen WARNING] iteration: 2, dip seq length: 4 [19:11:34.0304 dis_gen INFO] keys: ["5'b10111", "5'b00111"] [19:15:17.0710 dis_gen WARNING] there is no more dis(es) within boundary [19:16:28.0866 check_uc WARNING] there is no unique key! [19:16:29.0108 check_ce WARNING] found 1 DFFs and LATs [19:16:30.0503 check_ce WARNING] ce failed! Traceback (most recent call last): File "/usr/local/bin/sby", line 442, in task_retcode = run_job(task) File "/usr/local/bin/sby", line 399, in run_job job.run(setupmode) File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 684, in run self.taskloop() File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 278, in taskloop task.poll() File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 191, in poll self.handle_exit(self.p.returncode) File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 115, in handle_exit self.exit_callback(retcode) File "/usr/local/bin/../share/yosys/python3/sby_engine_aiger.py", line 141, in exit_callback2 assert task2_status == "FAIL" AssertionError [19:29:20.0767 check_umc WARNING] umc failed! [19:29:20.0768 perform WARNING] increase depth to 25 [19:34:57.0217 dis_gen WARNING] there is no more dis(es) within boundary [19:36:56.0004 check_uc WARNING] there is no unique key! [19:36:56.0250 check_ce WARNING] found 1 DFFs and LATs [19:36:57.0688 check_ce WARNING] ce failed! ... [20:44:05.0795 perform WARNING] increase depth to 40 [21:01:10.0395 dis_gen WARNING] there is no more dis(es) within boundary [21:07:11.0289 check_uc WARNING] there is no unique key! [21:07:11.0520 check_ce WARNING] found 1 DFFs and LATs [21:07:12.0960 check_ce WARNING] ce failed! [21:11:12.0246 main CRITICAL] timeout reached! [21:11:12.0249 execution_time WARNING] total time: 7200.10s

The reason for UMC check failure is because I only have 16GB of ram on this machine and it cannot complete the UMC check for this design. You can open system monitor to see if you hit %100 of your memory or not. If you hit that point in any run then smt engine will be killed by the OS.

[rafidmuttaki]

Hi, I will check that. My machine has 12 gb ram allocated. So, I think it is the problem you are mentioning here. My query is the design is a smaller one with very small key size. Is there a work around to get any solution here?

[shervinrs]

You can disable UMC check and continue the execution without that. If you have more than one key, then, the attack would not be able to terminate but it guarantees that for up to the current depth there is no other DIP and all the remaining keys are correct.

The other way would be to use a system with more memory. For large designs I have even used systems with 512GB of memory.

[rafidmuttaki]

Hello, I have one correct key combination for now. Where should I edit to disable the UMC check? In the future, I may consider moving to a larger memory.

[shervinrs]

Comment these lines from formal/seq_attack_formal.py

elif not self.config.enable_async:
  if self.check_ce():
      self.keys = self.find_keys()
      logging.warning("key: " + str(self.keys))
      return
  elif self.check_umc():
      self.keys = self.find_keys(equal_keys=True)
      logging.warning("key: " + str(self.keys))
      return

[rafidmuttaki]

Hi, I am having the attached errors while running the design. Can you please check. The uc passes and after that there comes an error. netlist.zip logfile.txt

[shervinrs]

It returns correctly on my machine with 16GB of ram. It is probably because of memory constraints. Check system monitor when it reaches that point.

[10:07:21.0412 verilog2circuit WARNING] circuit: aes_core_new, inputs: 390, outputs: 144, keyinputs: 0 [10:07:21.0420 verilog2circuit WARNING] circuit: aes_core_new_obf, inputs: 390, outputs: 144, keyinputs: 5 [10:07:21.0420 perform WARNING] initial values for boundary=20, step=10 [10:07:21.0420 perform WARNING] timeout=7200s [10:07:46.0141 dis_gen INFO] dip: ["389'b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001000", "389'b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001"] ... [10:17:35.0908 dis_gen WARNING] iteration: 4, dip seq length: 5 [10:17:35.0908 dis_gen INFO] keys: ["5'b01111", "5'b11111"] [10:18:37.0973 dis_gen WARNING] two different agreeing keys could not be found for the current set of assumptions, checking uc [10:19:46.0637 check_uc WARNING] uc passed! [10:30:33.0956 find_keys INFO] assigned keys: ["5'b11111", "5'b11111"] [10:30:33.0956 perform WARNING] key: 5'b11111 [10:30:33.0957 execution_time WARNING] total time: 1392.56s